Step | Hyp | Ref
| Expression |
1 | | projf1o.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | snidg 4206 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐴 ∈ {𝐴}) |
5 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
6 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐴 ∈ {𝐴} ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
7 | 4, 5, 6 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
8 | | projf1o.2 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) |
9 | | opeq2 4403 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈𝐴, 𝑥〉 = 〈𝐴, 𝑦〉) |
10 | 9 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) = (𝑦 ∈ 𝐵 ↦ 〈𝐴, 𝑦〉) |
11 | 8, 10 | eqtri 2644 |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ 〈𝐴, 𝑦〉) |
12 | 7, 11 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐵⟶({𝐴} × 𝐵)) |
13 | | simpl1 1064 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 𝜑) |
14 | 7 | elexd 3214 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ V) |
15 | 11 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ V) → (𝐹‘𝑦) = 〈𝐴, 𝑦〉) |
16 | 5, 14, 15 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) = 〈𝐴, 𝑦〉) |
17 | 16 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
18 | 17 | 3adant3 1081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
20 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → (𝐹‘𝑦) = (𝐹‘𝑧)) |
21 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 = (𝑦 ∈ 𝐵 ↦ 〈𝐴, 𝑦〉)) |
22 | | opeq2 4403 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑦 = 𝑧) → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
24 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
25 | | opex 4932 |
. . . . . . . . . . . . . 14
⊢
〈𝐴, 𝑧〉 ∈ V |
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 〈𝐴, 𝑧〉 ∈ V) |
27 | 21, 23, 24, 26 | fvmptd 6288 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
28 | 27 | 3adant2 1080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
29 | 28 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
30 | 19, 20, 29 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
31 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
32 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑧 ∈ V) |
34 | | opthg2 4948 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑧 ∈ V) → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
35 | 1, 33, 34 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
36 | 35 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
37 | 31, 36 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → (𝐴 = 𝐴 ∧ 𝑦 = 𝑧)) |
38 | 37 | simprd 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → 𝑦 = 𝑧) |
39 | 13, 30, 38 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 𝑦 = 𝑧) |
40 | 39 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
41 | 40 | 3expb 1266 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
42 | 41 | ralrimivva 2971 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
43 | 12, 42 | jca 554 |
. . . 4
⊢ (𝜑 → (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
44 | | dff13 6512 |
. . . 4
⊢ (𝐹:𝐵–1-1→({𝐴} × 𝐵) ↔ (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
45 | 43, 44 | sylibr 224 |
. . 3
⊢ (𝜑 → 𝐹:𝐵–1-1→({𝐴} × 𝐵)) |
46 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → 𝑧 ∈ ({𝐴} × 𝐵)) |
47 | | elsnxp 5677 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
48 | 1, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
49 | 48 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
50 | 46, 49 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉) |
51 | 16 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → (𝐹‘𝑦) = 〈𝐴, 𝑦〉) |
52 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = 〈𝐴, 𝑦〉) |
53 | 52 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝐴, 𝑦〉 → 〈𝐴, 𝑦〉 = 𝑧) |
54 | 53 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → 〈𝐴, 𝑦〉 = 𝑧) |
55 | 51, 54 | eqtr2d 2657 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → 𝑧 = (𝐹‘𝑦)) |
56 | 55 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = (𝐹‘𝑦))) |
57 | 56 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) ∧ 𝑦 ∈ 𝐵) → (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = (𝐹‘𝑦))) |
58 | 57 | reximdva 3017 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → (∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉 → ∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
59 | 50, 58 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦)) |
60 | 59 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦)) |
61 | 12, 60 | jca 554 |
. . . 4
⊢ (𝜑 → (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
62 | | dffo3 6374 |
. . . 4
⊢ (𝐹:𝐵–onto→({𝐴} × 𝐵) ↔ (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
63 | 61, 62 | sylibr 224 |
. . 3
⊢ (𝜑 → 𝐹:𝐵–onto→({𝐴} × 𝐵)) |
64 | 45, 63 | jca 554 |
. 2
⊢ (𝜑 → (𝐹:𝐵–1-1→({𝐴} × 𝐵) ∧ 𝐹:𝐵–onto→({𝐴} × 𝐵))) |
65 | | df-f1o 5895 |
. 2
⊢ (𝐹:𝐵–1-1-onto→({𝐴} × 𝐵) ↔ (𝐹:𝐵–1-1→({𝐴} × 𝐵) ∧ 𝐹:𝐵–onto→({𝐴} × 𝐵))) |
66 | 64, 65 | sylibr 224 |
1
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵)) |