| Step | Hyp | Ref
| Expression |
| 1 | | f1o2d2.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| 2 | | mpompts 8090 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶) |
| 3 | 1, 2 | eqtri 2765 |
. 2
⊢ 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶) |
| 4 | | xp1st 8046 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (1st ‘𝑤) ∈ 𝐴) |
| 5 | | xp2nd 8047 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) |
| 6 | | f1o2d2.r |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) |
| 7 | 6 | anassrs 467 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐷) |
| 8 | 7 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷) |
| 9 | | rspcsbela 4438 |
. . . . . 6
⊢
(((2nd ‘𝑤) ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 10 | 5, 8, 9 | syl2anr 597 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 11 | 10 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ∀𝑥 ∈ 𝐴 ⦋(2nd ‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 13 | | rspcsbela 4438 |
. . 3
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ⦋(2nd ‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) → ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 14 | 4, 12, 13 | syl2an2 686 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ∈ 𝐷) |
| 15 | | f1o2d2.i |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐼 ∈ 𝐴) |
| 16 | | f1o2d2.j |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐽 ∈ 𝐵) |
| 17 | 15, 16 | opelxpd 5724 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 〈𝐼, 𝐽〉 ∈ (𝐴 × 𝐵)) |
| 18 | 5 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → (2nd ‘𝑤) ∈ 𝐵) |
| 19 | | sbceq2g 4419 |
. . . . 5
⊢
((2nd ‘𝑤) ∈ 𝐵 → ([(2nd
‘𝑤) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → ([(2nd
‘𝑤) / 𝑦]𝑧 = 𝐶 ↔ 𝑧 = ⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 21 | 20 | sbcbidv 3845 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → ([(1st
‘𝑤) / 𝑥][(2nd
‘𝑤) / 𝑦]𝑧 = 𝐶 ↔ [(1st ‘𝑤) / 𝑥]𝑧 = ⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 22 | 4 | ad2antrl 728 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → (1st ‘𝑤) ∈ 𝐴) |
| 23 | 18 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ 𝑥 = (1st ‘𝑤)) → (2nd ‘𝑤) ∈ 𝐵) |
| 24 | | eqop 8056 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝑤 = 〈𝐼, 𝐽〉 ↔ ((1st ‘𝑤) = 𝐼 ∧ (2nd ‘𝑤) = 𝐽))) |
| 25 | 24 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → (𝑤 = 〈𝐼, 𝐽〉 ↔ ((1st ‘𝑤) = 𝐼 ∧ (2nd ‘𝑤) = 𝐽))) |
| 26 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = 𝐼 ↔ (1st ‘𝑤) = 𝐼)) |
| 27 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑤) → (𝑦 = 𝐽 ↔ (2nd ‘𝑤) = 𝐽)) |
| 28 | 26, 27 | bi2anan9 638 |
. . . . . . . . 9
⊢ ((𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ ((1st ‘𝑤) = 𝐼 ∧ (2nd ‘𝑤) = 𝐽))) |
| 29 | 28 | bicomd 223 |
. . . . . . . 8
⊢ ((𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → (((1st ‘𝑤) = 𝐼 ∧ (2nd ‘𝑤) = 𝐽) ↔ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))) |
| 30 | 25, 29 | sylan9bb 509 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ (𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤))) → (𝑤 = 〈𝐼, 𝐽〉 ↔ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))) |
| 31 | 30 | anassrs 467 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ 𝑥 = (1st ‘𝑤)) ∧ 𝑦 = (2nd ‘𝑤)) → (𝑤 = 〈𝐼, 𝐽〉 ↔ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))) |
| 32 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1st ‘𝑤) → (𝑥 ∈ 𝐴 ↔ (1st ‘𝑤) ∈ 𝐴)) |
| 33 | 4, 32 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝑥 = (1st ‘𝑤) → 𝑥 ∈ 𝐴)) |
| 34 | 33 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st ‘𝑤)) → 𝑥 ∈ 𝐴) |
| 35 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (2nd ‘𝑤) → (𝑦 ∈ 𝐵 ↔ (2nd ‘𝑤) ∈ 𝐵)) |
| 36 | 5, 35 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝑦 = (2nd ‘𝑤) → 𝑦 ∈ 𝐵)) |
| 37 | 36 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 = (2nd ‘𝑤)) → 𝑦 ∈ 𝐵) |
| 38 | 34, 37 | anim12dan 619 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤))) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 39 | 38 | 3impb 1115 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 40 | 39 | 3adant1r 1178 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 41 | | simp1r 1199 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → 𝑧 ∈ 𝐷) |
| 42 | 40, 41 | jca 511 |
. . . . . . . 8
⊢ (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) |
| 43 | | f1o2d2.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶)) |
| 44 | 42, 43 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷) ∧ 𝑥 = (1st ‘𝑤) ∧ 𝑦 = (2nd ‘𝑤))) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶)) |
| 45 | 44 | 3anassrs 1361 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ 𝑥 = (1st ‘𝑤)) ∧ 𝑦 = (2nd ‘𝑤)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶)) |
| 46 | 31, 45 | bitr2d 280 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ 𝑥 = (1st ‘𝑤)) ∧ 𝑦 = (2nd ‘𝑤)) → (𝑧 = 𝐶 ↔ 𝑤 = 〈𝐼, 𝐽〉)) |
| 47 | 23, 46 | sbcied 3832 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) ∧ 𝑥 = (1st ‘𝑤)) → ([(2nd
‘𝑤) / 𝑦]𝑧 = 𝐶 ↔ 𝑤 = 〈𝐼, 𝐽〉)) |
| 48 | 22, 47 | sbcied 3832 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → ([(1st
‘𝑤) / 𝑥][(2nd
‘𝑤) / 𝑦]𝑧 = 𝐶 ↔ 𝑤 = 〈𝐼, 𝐽〉)) |
| 49 | | sbceq2g 4419 |
. . . 4
⊢
((1st ‘𝑤) ∈ 𝐴 → ([(1st
‘𝑤) / 𝑥]𝑧 = ⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 50 | 22, 49 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → ([(1st
‘𝑤) / 𝑥]𝑧 = ⦋(2nd
‘𝑤) / 𝑦⦌𝐶 ↔ 𝑧 = ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 51 | 21, 48, 50 | 3bitr3d 309 |
. 2
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧 ∈ 𝐷)) → (𝑤 = 〈𝐼, 𝐽〉 ↔ 𝑧 = ⦋(1st
‘𝑤) / 𝑥⦌⦋(2nd
‘𝑤) / 𝑦⦌𝐶)) |
| 52 | 3, 14, 17, 51 | f1o2d 7687 |
1
⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) |