| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xpsfrnel2 17610 | . . . . . 6
⊢
({〈∅, 𝑥〉, 〈1o, 𝑦〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | 
| 2 | 1 | biimpri 228 | . . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {〈∅, 𝑥〉, 〈1o, 𝑦〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵)) | 
| 3 | 2 | rgen2 3198 | . . . 4
⊢
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 {〈∅, 𝑥〉, 〈1o, 𝑦〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) | 
| 4 |  | xpsff1o.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 5 | 4 | fmpo 8094 | . . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 {〈∅, 𝑥〉, 〈1o, 𝑦〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)) | 
| 6 | 3, 5 | mpbi 230 | . . 3
⊢ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | 
| 7 |  | 1st2nd2 8054 | . . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 8 | 7 | fveq2d 6909 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 9 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑧)𝐹(2nd ‘𝑧)) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 10 |  | xp1st 8047 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (1st ‘𝑧) ∈ 𝐴) | 
| 11 |  | xp2nd 8048 | . . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) | 
| 12 | 4 | xpsfval 17612 | . . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {〈∅, (1st
‘𝑧)〉,
〈1o, (2nd ‘𝑧)〉}) | 
| 13 | 10, 11, 12 | syl2anc 584 | . . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {〈∅, (1st
‘𝑧)〉,
〈1o, (2nd ‘𝑧)〉}) | 
| 14 | 9, 13 | eqtr3id 2790 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) = {〈∅,
(1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}) | 
| 15 | 8, 14 | eqtrd 2776 | . . . . . 6
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = {〈∅, (1st
‘𝑧)〉,
〈1o, (2nd ‘𝑧)〉}) | 
| 16 |  | 1st2nd2 8054 | . . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 17 | 16 | fveq2d 6909 | . . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 18 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑤)𝐹(2nd ‘𝑤)) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 19 |  | xp1st 8047 | . . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (1st ‘𝑤) ∈ 𝐴) | 
| 20 |  | xp2nd 8048 | . . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) | 
| 21 | 4 | xpsfval 17612 | . . . . . . . . 9
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (2nd ‘𝑤) ∈ 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {〈∅, (1st
‘𝑤)〉,
〈1o, (2nd ‘𝑤)〉}) | 
| 22 | 19, 20, 21 | syl2anc 584 | . . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {〈∅, (1st
‘𝑤)〉,
〈1o, (2nd ‘𝑤)〉}) | 
| 23 | 18, 22 | eqtr3id 2790 | . . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) = {〈∅,
(1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}) | 
| 24 | 17, 23 | eqtrd 2776 | . . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = {〈∅, (1st
‘𝑤)〉,
〈1o, (2nd ‘𝑤)〉}) | 
| 25 | 15, 24 | eqeqan12d 2750 | . . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {〈∅, (1st
‘𝑧)〉,
〈1o, (2nd ‘𝑧)〉} = {〈∅, (1st
‘𝑤)〉,
〈1o, (2nd ‘𝑤)〉})) | 
| 26 |  | fveq1 6904 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉} =
{〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉} →
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘∅) = ({〈∅,
(1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘∅)) | 
| 27 |  | fvex 6918 | . . . . . . . . 9
⊢
(1st ‘𝑧) ∈ V | 
| 28 |  | fvpr0o 17605 | . . . . . . . . 9
⊢
((1st ‘𝑧) ∈ V → ({〈∅,
(1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘∅) = (1st
‘𝑧)) | 
| 29 | 27, 28 | ax-mp 5 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘∅) = (1st
‘𝑧) | 
| 30 |  | fvex 6918 | . . . . . . . . 9
⊢
(1st ‘𝑤) ∈ V | 
| 31 |  | fvpr0o 17605 | . . . . . . . . 9
⊢
((1st ‘𝑤) ∈ V → ({〈∅,
(1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘∅) = (1st
‘𝑤)) | 
| 32 | 30, 31 | ax-mp 5 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘∅) = (1st
‘𝑤) | 
| 33 | 26, 29, 32 | 3eqtr3g 2799 | . . . . . . 7
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉} =
{〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉} →
(1st ‘𝑧) =
(1st ‘𝑤)) | 
| 34 |  | fveq1 6904 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉} =
{〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉} →
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘1o) =
({〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘1o)) | 
| 35 |  | fvex 6918 | . . . . . . . . 9
⊢
(2nd ‘𝑧) ∈ V | 
| 36 |  | fvpr1o 17606 | . . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ V → ({〈∅,
(1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘1o) =
(2nd ‘𝑧)) | 
| 37 | 35, 36 | ax-mp 5 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉}‘1o) =
(2nd ‘𝑧) | 
| 38 |  | fvex 6918 | . . . . . . . . 9
⊢
(2nd ‘𝑤) ∈ V | 
| 39 |  | fvpr1o 17606 | . . . . . . . . 9
⊢
((2nd ‘𝑤) ∈ V → ({〈∅,
(1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘1o) =
(2nd ‘𝑤)) | 
| 40 | 38, 39 | ax-mp 5 | . . . . . . . 8
⊢
({〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉}‘1o) =
(2nd ‘𝑤) | 
| 41 | 34, 37, 40 | 3eqtr3g 2799 | . . . . . . 7
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉} =
{〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉} →
(2nd ‘𝑧) =
(2nd ‘𝑤)) | 
| 42 | 33, 41 | opeq12d 4880 | . . . . . 6
⊢
({〈∅, (1st ‘𝑧)〉, 〈1o, (2nd
‘𝑧)〉} =
{〈∅, (1st ‘𝑤)〉, 〈1o, (2nd
‘𝑤)〉} →
〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 43 | 7, 16 | eqeqan12d 2750 | . . . . . 6
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (𝑧 = 𝑤 ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉)) | 
| 44 | 42, 43 | imbitrrid 246 | . . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ({〈∅, (1st
‘𝑧)〉,
〈1o, (2nd ‘𝑧)〉} = {〈∅, (1st
‘𝑤)〉,
〈1o, (2nd ‘𝑤)〉} → 𝑧 = 𝑤)) | 
| 45 | 25, 44 | sylbid 240 | . . . 4
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) | 
| 46 | 45 | rgen2 3198 | . . 3
⊢
∀𝑧 ∈
(𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) | 
| 47 |  | dff13 7276 | . . 3
⊢ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) | 
| 48 | 6, 46, 47 | mpbir2an 711 | . 2
⊢ 𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | 
| 49 |  | xpsfrnel 17608 | . . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑧 Fn 2o ∧ (𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵)) | 
| 50 | 49 | simp2bi 1146 | . . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘∅) ∈ 𝐴) | 
| 51 | 49 | simp3bi 1147 | . . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘1o) ∈ 𝐵) | 
| 52 | 4 | xpsfval 17612 | . . . . . . 7
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = {〈∅,
(𝑧‘∅)〉,
〈1o, (𝑧‘1o)〉}) | 
| 53 | 50, 51, 52 | syl2anc 584 | . . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = {〈∅,
(𝑧‘∅)〉,
〈1o, (𝑧‘1o)〉}) | 
| 54 |  | ixpfn 8944 | . . . . . . 7
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 Fn 2o) | 
| 55 |  | xpsfeq 17609 | . . . . . . 7
⊢ (𝑧 Fn 2o →
{〈∅, (𝑧‘∅)〉, 〈1o,
(𝑧‘1o)〉} = 𝑧) | 
| 56 | 54, 55 | syl 17 | . . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → {〈∅, (𝑧‘∅)〉,
〈1o, (𝑧‘1o)〉} = 𝑧) | 
| 57 | 53, 56 | eqtr2d 2777 | . . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) | 
| 58 |  | rspceov 7481 | . . . . 5
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵 ∧ 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) | 
| 59 | 50, 51, 57, 58 | syl3anc 1372 | . . . 4
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) | 
| 60 | 59 | rgen 3062 | . . 3
⊢
∀𝑧 ∈
X 𝑘
∈ 2o if(𝑘 =
∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏) | 
| 61 |  | foov 7608 | . . 3
⊢ (𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ X 𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏))) | 
| 62 | 6, 60, 61 | mpbir2an 711 | . 2
⊢ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | 
| 63 |  | df-f1o 6567 | . 2
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵))) | 
| 64 | 48, 62, 63 | mpbir2an 711 | 1
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) |