| Step | Hyp | Ref
| Expression |
| 1 | | simp3 1139 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑋 ≈ 𝑌) |
| 2 | | bren 8995 |
. . 3
⊢ (𝑋 ≈ 𝑌 ↔ ∃𝑔 𝑔:𝑋–1-1-onto→𝑌) |
| 3 | 1, 2 | sylib 218 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑔 𝑔:𝑋–1-1-onto→𝑌) |
| 4 | | relen 8990 |
. . . . . . . 8
⊢ Rel
≈ |
| 5 | 4 | brrelex2i 5742 |
. . . . . . 7
⊢ (𝑋 ≈ 𝑌 → 𝑌 ∈ V) |
| 6 | 5 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → 𝑌 ∈ V) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑌 ∈ V) |
| 8 | | f1of 6848 |
. . . . . . 7
⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔:𝑋⟶𝑌) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝑔:𝑋⟶𝑌) |
| 10 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐴 ∈ 𝑋) |
| 11 | 9, 10 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑔‘𝐴) ∈ 𝑌) |
| 12 | | simpl2 1193 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → 𝐵 ∈ 𝑌) |
| 13 | | difsnen 9093 |
. . . . 5
⊢ ((𝑌 ∈ V ∧ (𝑔‘𝐴) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵})) |
| 14 | 7, 11, 12, 13 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵})) |
| 15 | | bren 8995 |
. . . 4
⊢ ((𝑌 ∖ {(𝑔‘𝐴)}) ≈ (𝑌 ∖ {𝐵}) ↔ ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) |
| 16 | 14, 15 | sylib 218 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) |
| 17 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑔‘𝐴) ∈ V |
| 18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ V) |
| 19 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐵 ∈ 𝑌) |
| 20 | | f1osng 6889 |
. . . . . . . . . 10
⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → {〈(𝑔‘𝐴), 𝐵〉}:{(𝑔‘𝐴)}–1-1-onto→{𝐵}) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {〈(𝑔‘𝐴), 𝐵〉}:{(𝑔‘𝐴)}–1-1-onto→{𝐵}) |
| 22 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) |
| 23 | | disjdif 4472 |
. . . . . . . . . 10
⊢ ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ |
| 24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅) |
| 25 | | disjdif 4472 |
. . . . . . . . . 10
⊢ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅ |
| 26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅) |
| 27 | | f1oun 6867 |
. . . . . . . . 9
⊢
((({〈(𝑔‘𝐴), 𝐵〉}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵})) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ ({𝐵} ∩ (𝑌 ∖ {𝐵})) = ∅)) → ({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵}))) |
| 28 | 21, 22, 24, 26, 27 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵}))) |
| 29 | 8 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋⟶𝑌) |
| 30 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝐴 ∈ 𝑋) |
| 31 | 29, 30 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ 𝑌) |
| 32 | | uncom 4158 |
. . . . . . . . . . 11
⊢ ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) |
| 33 | | difsnid 4810 |
. . . . . . . . . . 11
⊢ ((𝑔‘𝐴) ∈ 𝑌 → ((𝑌 ∖ {(𝑔‘𝐴)}) ∪ {(𝑔‘𝐴)}) = 𝑌) |
| 34 | 32, 33 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝑔‘𝐴) ∈ 𝑌 → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌) |
| 35 | 31, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌) |
| 36 | | uncom 4158 |
. . . . . . . . . . 11
⊢ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = ((𝑌 ∖ {𝐵}) ∪ {𝐵}) |
| 37 | | difsnid 4810 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑌 → ((𝑌 ∖ {𝐵}) ∪ {𝐵}) = 𝑌) |
| 38 | 36, 37 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑌 → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) |
| 39 | 19, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) |
| 40 | | f1oeq23 6839 |
. . . . . . . . 9
⊢
((({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)})) = 𝑌 ∧ ({𝐵} ∪ (𝑌 ∖ {𝐵})) = 𝑌) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):𝑌–1-1-onto→𝑌)) |
| 41 | 35, 39, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):({(𝑔‘𝐴)} ∪ (𝑌 ∖ {(𝑔‘𝐴)}))–1-1-onto→({𝐵} ∪ (𝑌 ∖ {𝐵})) ↔ ({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):𝑌–1-1-onto→𝑌)) |
| 42 | 28, 41 | mpbid 232 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):𝑌–1-1-onto→𝑌) |
| 43 | | simprl 771 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔:𝑋–1-1-onto→𝑌) |
| 44 | | f1oco 6871 |
. . . . . . 7
⊢
((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ):𝑌–1-1-onto→𝑌 ∧ 𝑔:𝑋–1-1-onto→𝑌) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌) |
| 45 | 42, 43, 44 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌) |
| 46 | | f1ofn 6849 |
. . . . . . . . 9
⊢ (𝑔:𝑋–1-1-onto→𝑌 → 𝑔 Fn 𝑋) |
| 47 | 46 | ad2antrl 728 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → 𝑔 Fn 𝑋) |
| 48 | | fvco2 7006 |
. . . . . . . 8
⊢ ((𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ)‘(𝑔‘𝐴))) |
| 49 | 47, 30, 48 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ)‘(𝑔‘𝐴))) |
| 50 | | f1ofn 6849 |
. . . . . . . . 9
⊢
({〈(𝑔‘𝐴), 𝐵〉}:{(𝑔‘𝐴)}–1-1-onto→{𝐵} → {〈(𝑔‘𝐴), 𝐵〉} Fn {(𝑔‘𝐴)}) |
| 51 | 21, 50 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → {〈(𝑔‘𝐴), 𝐵〉} Fn {(𝑔‘𝐴)}) |
| 52 | | f1ofn 6849 |
. . . . . . . . 9
⊢ (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)})) |
| 53 | 52 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)})) |
| 54 | 17 | snid 4662 |
. . . . . . . . 9
⊢ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)} |
| 55 | 54 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (𝑔‘𝐴) ∈ {(𝑔‘𝐴)}) |
| 56 | | fvun1 7000 |
. . . . . . . 8
⊢
(({〈(𝑔‘𝐴), 𝐵〉} Fn {(𝑔‘𝐴)} ∧ ℎ Fn (𝑌 ∖ {(𝑔‘𝐴)}) ∧ (({(𝑔‘𝐴)} ∩ (𝑌 ∖ {(𝑔‘𝐴)})) = ∅ ∧ (𝑔‘𝐴) ∈ {(𝑔‘𝐴)})) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ)‘(𝑔‘𝐴)) = ({〈(𝑔‘𝐴), 𝐵〉}‘(𝑔‘𝐴))) |
| 57 | 51, 53, 24, 55, 56 | syl112anc 1376 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ)‘(𝑔‘𝐴)) = ({〈(𝑔‘𝐴), 𝐵〉}‘(𝑔‘𝐴))) |
| 58 | | fvsng 7200 |
. . . . . . . 8
⊢ (((𝑔‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑌) → ({〈(𝑔‘𝐴), 𝐵〉}‘(𝑔‘𝐴)) = 𝐵) |
| 59 | 18, 19, 58 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ({〈(𝑔‘𝐴), 𝐵〉}‘(𝑔‘𝐴)) = 𝐵) |
| 60 | 49, 57, 59 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) |
| 61 | | snex 5436 |
. . . . . . . . 9
⊢
{〈(𝑔‘𝐴), 𝐵〉} ∈ V |
| 62 | | vex 3484 |
. . . . . . . . 9
⊢ ℎ ∈ V |
| 63 | 61, 62 | unex 7764 |
. . . . . . . 8
⊢
({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∈ V |
| 64 | | vex 3484 |
. . . . . . . 8
⊢ 𝑔 ∈ V |
| 65 | 63, 64 | coex 7952 |
. . . . . . 7
⊢
(({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔) ∈ V |
| 66 | | f1oeq1 6836 |
. . . . . . . 8
⊢ (𝑓 = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔) → (𝑓:𝑋–1-1-onto→𝑌 ↔ (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌)) |
| 67 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔) → (𝑓‘𝐴) = ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴)) |
| 68 | 67 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑓 = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔) → ((𝑓‘𝐴) = 𝐵 ↔ ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵)) |
| 69 | 66, 68 | anbi12d 632 |
. . . . . . 7
⊢ (𝑓 = (({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵) ↔ ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵))) |
| 70 | 65, 69 | spcev 3606 |
. . . . . 6
⊢
(((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔):𝑋–1-1-onto→𝑌 ∧ ((({〈(𝑔‘𝐴), 𝐵〉} ∪ ℎ) ∘ 𝑔)‘𝐴) = 𝐵) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)) |
| 71 | 45, 60, 70 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ (𝑔:𝑋–1-1-onto→𝑌 ∧ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}))) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)) |
| 72 | 71 | expr 456 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))) |
| 73 | 72 | exlimdv 1933 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → (∃ℎ ℎ:(𝑌 ∖ {(𝑔‘𝐴)})–1-1-onto→(𝑌 ∖ {𝐵}) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵))) |
| 74 | 16, 73 | mpd 15 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) ∧ 𝑔:𝑋–1-1-onto→𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)) |
| 75 | 3, 74 | exlimddv 1935 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)) |