Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → 𝑋 ≈ 𝑌 ) |
2 |
|
bren |
⊢ ( 𝑋 ≈ 𝑌 ↔ ∃ 𝑔 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) |
3 |
1 2
|
sylib |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → ∃ 𝑔 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) |
4 |
|
relen |
⊢ Rel ≈ |
5 |
4
|
brrelex2i |
⊢ ( 𝑋 ≈ 𝑌 → 𝑌 ∈ V ) |
6 |
5
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → 𝑌 ∈ V ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑌 ∈ V ) |
8 |
|
f1of |
⊢ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 → 𝑔 : 𝑋 ⟶ 𝑌 ) |
9 |
8
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑔 : 𝑋 ⟶ 𝑌 ) |
10 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐴 ∈ 𝑋 ) |
11 |
9 10
|
ffvelrnd |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 ) |
12 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐵 ∈ 𝑌 ) |
13 |
|
difsnen |
⊢ ( ( 𝑌 ∈ V ∧ ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) ) |
14 |
7 11 12 13
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) ) |
15 |
|
bren |
⊢ ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ≈ ( 𝑌 ∖ { 𝐵 } ) ↔ ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) |
16 |
14 15
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) |
17 |
|
fvex |
⊢ ( 𝑔 ‘ 𝐴 ) ∈ V |
18 |
17
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ V ) |
19 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝐵 ∈ 𝑌 ) |
20 |
|
f1osng |
⊢ ( ( ( 𝑔 ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } ) |
21 |
18 19 20
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } ) |
22 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) |
23 |
|
disjdif |
⊢ ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ |
24 |
23
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ ) |
25 |
|
disjdif |
⊢ ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅ |
26 |
25
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅ ) |
27 |
|
f1oun |
⊢ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ∧ ( ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ ∧ ( { 𝐵 } ∩ ( 𝑌 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ) |
28 |
21 22 24 26 27
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ) |
29 |
8
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 : 𝑋 ⟶ 𝑌 ) |
30 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝐴 ∈ 𝑋 ) |
31 |
29 30
|
ffvelrnd |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 ) |
32 |
|
uncom |
⊢ ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∪ { ( 𝑔 ‘ 𝐴 ) } ) |
33 |
|
difsnid |
⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 → ( ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∪ { ( 𝑔 ‘ 𝐴 ) } ) = 𝑌 ) |
34 |
32 33
|
eqtrid |
⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ 𝑌 → ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 ) |
35 |
31 34
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 ) |
36 |
|
uncom |
⊢ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } ) |
37 |
|
difsnid |
⊢ ( 𝐵 ∈ 𝑌 → ( ( 𝑌 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝑌 ) |
38 |
36 37
|
eqtrid |
⊢ ( 𝐵 ∈ 𝑌 → ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 ) |
39 |
19 38
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 ) |
40 |
|
f1oeq23 |
⊢ ( ( ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = 𝑌 ∧ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) = 𝑌 ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ↔ ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ) ) |
41 |
35 39 40
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : ( { ( 𝑔 ‘ 𝐴 ) } ∪ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) –1-1-onto→ ( { 𝐵 } ∪ ( 𝑌 ∖ { 𝐵 } ) ) ↔ ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ) ) |
42 |
28 41
|
mpbid |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ) |
43 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) |
44 |
|
f1oco |
⊢ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) : 𝑌 –1-1-onto→ 𝑌 ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ) |
45 |
42 43 44
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ) |
46 |
|
f1ofn |
⊢ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 → 𝑔 Fn 𝑋 ) |
47 |
46
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → 𝑔 Fn 𝑋 ) |
48 |
|
fvco2 |
⊢ ( ( 𝑔 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) ) |
49 |
47 30 48
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) ) |
50 |
|
f1ofn |
⊢ ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } : { ( 𝑔 ‘ 𝐴 ) } –1-1-onto→ { 𝐵 } → { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } Fn { ( 𝑔 ‘ 𝐴 ) } ) |
51 |
21 50
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } Fn { ( 𝑔 ‘ 𝐴 ) } ) |
52 |
|
f1ofn |
⊢ ( ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) |
53 |
52
|
ad2antll |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) |
54 |
17
|
snid |
⊢ ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) } |
55 |
54
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) } ) |
56 |
|
fvun1 |
⊢ ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } Fn { ( 𝑔 ‘ 𝐴 ) } ∧ ℎ Fn ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ∧ ( ( { ( 𝑔 ‘ 𝐴 ) } ∩ ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) ) = ∅ ∧ ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑔 ‘ 𝐴 ) } ) ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) = ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ‘ ( 𝑔 ‘ 𝐴 ) ) ) |
57 |
51 53 24 55 56
|
syl112anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ‘ ( 𝑔 ‘ 𝐴 ) ) = ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ‘ ( 𝑔 ‘ 𝐴 ) ) ) |
58 |
|
fvsng |
⊢ ( ( ( 𝑔 ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ‘ ( 𝑔 ‘ 𝐴 ) ) = 𝐵 ) |
59 |
18 19 58
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ‘ ( 𝑔 ‘ 𝐴 ) ) = 𝐵 ) |
60 |
49 57 59
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) |
61 |
|
snex |
⊢ { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∈ V |
62 |
|
vex |
⊢ ℎ ∈ V |
63 |
61 62
|
unex |
⊢ ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∈ V |
64 |
|
vex |
⊢ 𝑔 ∈ V |
65 |
63 64
|
coex |
⊢ ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ∈ V |
66 |
|
f1oeq1 |
⊢ ( 𝑓 = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) → ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ↔ ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ) ) |
67 |
|
fveq1 |
⊢ ( 𝑓 = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) → ( 𝑓 ‘ 𝐴 ) = ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) ) |
68 |
67
|
eqeq1d |
⊢ ( 𝑓 = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) → ( ( 𝑓 ‘ 𝐴 ) = 𝐵 ↔ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) ) |
69 |
66 68
|
anbi12d |
⊢ ( 𝑓 = ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) → ( ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ↔ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) ) ) |
70 |
65 69
|
spcev |
⊢ ( ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) : 𝑋 –1-1-onto→ 𝑌 ∧ ( ( ( { 〈 ( 𝑔 ‘ 𝐴 ) , 𝐵 〉 } ∪ ℎ ) ∘ 𝑔 ) ‘ 𝐴 ) = 𝐵 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) |
71 |
45 60 70
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ ( 𝑔 : 𝑋 –1-1-onto→ 𝑌 ∧ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) |
72 |
71
|
expr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) ) |
73 |
72
|
exlimdv |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ( ∃ ℎ ℎ : ( 𝑌 ∖ { ( 𝑔 ‘ 𝐴 ) } ) –1-1-onto→ ( 𝑌 ∖ { 𝐵 } ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) ) |
74 |
16 73
|
mpd |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) ∧ 𝑔 : 𝑋 –1-1-onto→ 𝑌 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) |
75 |
3 74
|
exlimddv |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌 ) → ∃ 𝑓 ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑓 ‘ 𝐴 ) = 𝐵 ) ) |