Step | Hyp | Ref
| Expression |
1 | | projf1o.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | snidg 4429 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
4 | 3 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐴 ∈ {𝐴}) |
5 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
6 | | opelxpi 5383 |
. . . . . . 7
⊢ ((𝐴 ∈ {𝐴} ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
7 | 4, 5, 6 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
8 | | projf1o.2 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) |
9 | | opeq2 4626 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈𝐴, 𝑥〉 = 〈𝐴, 𝑦〉) |
10 | 9 | cbvmptv 4975 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) = (𝑦 ∈ 𝐵 ↦ 〈𝐴, 𝑦〉) |
11 | 8, 10 | eqtri 2849 |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ 〈𝐴, 𝑦〉) |
12 | 7, 11 | fmptd 6638 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐵⟶({𝐴} × 𝐵)) |
13 | | simpl1 1246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 𝜑) |
14 | 8, 9, 5, 7 | fvmptd3 6555 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) = 〈𝐴, 𝑦〉) |
15 | 14 | eqcomd 2831 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
16 | 15 | 3adant3 1166 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
17 | 16 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 〈𝐴, 𝑦〉 = (𝐹‘𝑦)) |
18 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → (𝐹‘𝑦) = (𝐹‘𝑧)) |
19 | | opeq2 4626 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
20 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
21 | | opex 5155 |
. . . . . . . . . . . . . 14
⊢
〈𝐴, 𝑧〉 ∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 〈𝐴, 𝑧〉 ∈ V) |
23 | 11, 19, 20, 22 | fvmptd3 6555 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
24 | 23 | 3adant2 1165 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
25 | 24 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → (𝐹‘𝑧) = 〈𝐴, 𝑧〉) |
26 | 17, 18, 25 | 3eqtrd 2865 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
27 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) |
28 | | vex 3417 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
29 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑧 ∈ V) |
30 | | opthg2 5170 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑧 ∈ V) → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
31 | 1, 29, 30 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
32 | 31 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → (〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉 ↔ (𝐴 = 𝐴 ∧ 𝑦 = 𝑧))) |
33 | 27, 32 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → (𝐴 = 𝐴 ∧ 𝑦 = 𝑧)) |
34 | 33 | simprd 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 〈𝐴, 𝑦〉 = 〈𝐴, 𝑧〉) → 𝑦 = 𝑧) |
35 | 13, 26, 34 | syl2anc 579 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝐹‘𝑦) = (𝐹‘𝑧)) → 𝑦 = 𝑧) |
36 | 35 | ex 403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
37 | 36 | 3expb 1153 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
38 | 37 | ralrimivva 3180 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
39 | 12, 38 | jca 507 |
. . . 4
⊢ (𝜑 → (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
40 | | dff13 6772 |
. . . 4
⊢ (𝐹:𝐵–1-1→({𝐴} × 𝐵) ↔ (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
41 | 39, 40 | sylibr 226 |
. . 3
⊢ (𝜑 → 𝐹:𝐵–1-1→({𝐴} × 𝐵)) |
42 | | simpr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → 𝑧 ∈ ({𝐴} × 𝐵)) |
43 | | elsnxp 5922 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
44 | 1, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
45 | 44 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → (𝑧 ∈ ({𝐴} × 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉)) |
46 | 42, 45 | mpbid 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → ∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉) |
47 | 14 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → (𝐹‘𝑦) = 〈𝐴, 𝑦〉) |
48 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = 〈𝐴, 𝑦〉) |
49 | 48 | eqcomd 2831 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝐴, 𝑦〉 → 〈𝐴, 𝑦〉 = 𝑧) |
50 | 49 | adantl 475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → 〈𝐴, 𝑦〉 = 𝑧) |
51 | 47, 50 | eqtr2d 2862 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 〈𝐴, 𝑦〉) → 𝑧 = (𝐹‘𝑦)) |
52 | 51 | ex 403 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = (𝐹‘𝑦))) |
53 | 52 | adantlr 706 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) ∧ 𝑦 ∈ 𝐵) → (𝑧 = 〈𝐴, 𝑦〉 → 𝑧 = (𝐹‘𝑦))) |
54 | 53 | reximdva 3225 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → (∃𝑦 ∈ 𝐵 𝑧 = 〈𝐴, 𝑦〉 → ∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
55 | 46, 54 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ({𝐴} × 𝐵)) → ∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦)) |
56 | 55 | ralrimiva 3175 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦)) |
57 | 12, 56 | jca 507 |
. . . 4
⊢ (𝜑 → (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
58 | | dffo3 6628 |
. . . 4
⊢ (𝐹:𝐵–onto→({𝐴} × 𝐵) ↔ (𝐹:𝐵⟶({𝐴} × 𝐵) ∧ ∀𝑧 ∈ ({𝐴} × 𝐵)∃𝑦 ∈ 𝐵 𝑧 = (𝐹‘𝑦))) |
59 | 57, 58 | sylibr 226 |
. . 3
⊢ (𝜑 → 𝐹:𝐵–onto→({𝐴} × 𝐵)) |
60 | 41, 59 | jca 507 |
. 2
⊢ (𝜑 → (𝐹:𝐵–1-1→({𝐴} × 𝐵) ∧ 𝐹:𝐵–onto→({𝐴} × 𝐵))) |
61 | | df-f1o 6134 |
. 2
⊢ (𝐹:𝐵–1-1-onto→({𝐴} × 𝐵) ↔ (𝐹:𝐵–1-1→({𝐴} × 𝐵) ∧ 𝐹:𝐵–onto→({𝐴} × 𝐵))) |
62 | 60, 61 | sylibr 226 |
1
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵)) |