Step |
Hyp |
Ref |
Expression |
1 |
|
relsdom |
⊢ Rel ≺ |
2 |
1
|
brrelex2i |
⊢ ( ∅ ≺ 𝐵 → 𝐵 ∈ V ) |
3 |
|
0sdomg |
⊢ ( 𝐵 ∈ V → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) ) |
4 |
|
n0 |
⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐵 ) |
5 |
3 4
|
bitrdi |
⊢ ( 𝐵 ∈ V → ( ∅ ≺ 𝐵 ↔ ∃ 𝑧 𝑧 ∈ 𝐵 ) ) |
6 |
2 5
|
syl |
⊢ ( ∅ ≺ 𝐵 → ( ∅ ≺ 𝐵 ↔ ∃ 𝑧 𝑧 ∈ 𝐵 ) ) |
7 |
6
|
ibi |
⊢ ( ∅ ≺ 𝐵 → ∃ 𝑧 𝑧 ∈ 𝐵 ) |
8 |
|
domfi |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin ) |
9 |
|
simpl |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ∈ Fin ) |
10 |
|
brdomi |
⊢ ( 𝐵 ≼ 𝐴 → ∃ 𝑔 𝑔 : 𝐵 –1-1→ 𝐴 ) |
11 |
|
f1fn |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → 𝑔 Fn 𝐵 ) |
12 |
|
fnfi |
⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin ) → 𝑔 ∈ Fin ) |
13 |
11 12
|
sylan |
⊢ ( ( 𝑔 : 𝐵 –1-1→ 𝐴 ∧ 𝐵 ∈ Fin ) → 𝑔 ∈ Fin ) |
14 |
13
|
ex |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( 𝐵 ∈ Fin → 𝑔 ∈ Fin ) ) |
15 |
|
cnvfi |
⊢ ( 𝑔 ∈ Fin → ◡ 𝑔 ∈ Fin ) |
16 |
|
diffi |
⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ ran 𝑔 ) ∈ Fin ) |
17 |
|
snfi |
⊢ { 𝑧 } ∈ Fin |
18 |
|
xpfi |
⊢ ( ( ( 𝐴 ∖ ran 𝑔 ) ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ∈ Fin ) |
19 |
16 17 18
|
sylancl |
⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ∈ Fin ) |
20 |
|
unfi |
⊢ ( ( ◡ 𝑔 ∈ Fin ∧ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ∈ Fin ) → ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ∈ Fin ) |
21 |
15 19 20
|
syl2an |
⊢ ( ( 𝑔 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ∈ Fin ) |
22 |
|
df-f1 |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 ↔ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑔 ) ) |
23 |
22
|
simprbi |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → Fun ◡ 𝑔 ) |
24 |
|
vex |
⊢ 𝑧 ∈ V |
25 |
24
|
fconst |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) : ( 𝐴 ∖ ran 𝑔 ) ⟶ { 𝑧 } |
26 |
|
ffun |
⊢ ( ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) : ( 𝐴 ∖ ran 𝑔 ) ⟶ { 𝑧 } → Fun ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) |
27 |
25 26
|
ax-mp |
⊢ Fun ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) |
28 |
23 27
|
jctir |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( Fun ◡ 𝑔 ∧ Fun ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ) |
29 |
|
df-rn |
⊢ ran 𝑔 = dom ◡ 𝑔 |
30 |
29
|
eqcomi |
⊢ dom ◡ 𝑔 = ran 𝑔 |
31 |
24
|
snnz |
⊢ { 𝑧 } ≠ ∅ |
32 |
|
dmxp |
⊢ ( { 𝑧 } ≠ ∅ → dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ( 𝐴 ∖ ran 𝑔 ) ) |
33 |
31 32
|
ax-mp |
⊢ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ( 𝐴 ∖ ran 𝑔 ) |
34 |
30 33
|
ineq12i |
⊢ ( dom ◡ 𝑔 ∩ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( ran 𝑔 ∩ ( 𝐴 ∖ ran 𝑔 ) ) |
35 |
|
disjdif |
⊢ ( ran 𝑔 ∩ ( 𝐴 ∖ ran 𝑔 ) ) = ∅ |
36 |
34 35
|
eqtri |
⊢ ( dom ◡ 𝑔 ∩ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ∅ |
37 |
|
funun |
⊢ ( ( ( Fun ◡ 𝑔 ∧ Fun ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ∧ ( dom ◡ 𝑔 ∩ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ∅ ) → Fun ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ) |
38 |
28 36 37
|
sylancl |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → Fun ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ) |
39 |
38
|
adantl |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → Fun ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ) |
40 |
|
dmun |
⊢ dom ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( dom ◡ 𝑔 ∪ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) |
41 |
29
|
uneq1i |
⊢ ( ran 𝑔 ∪ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( dom ◡ 𝑔 ∪ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) |
42 |
33
|
uneq2i |
⊢ ( ran 𝑔 ∪ dom ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( ran 𝑔 ∪ ( 𝐴 ∖ ran 𝑔 ) ) |
43 |
40 41 42
|
3eqtr2i |
⊢ dom ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( ran 𝑔 ∪ ( 𝐴 ∖ ran 𝑔 ) ) |
44 |
|
f1f |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → 𝑔 : 𝐵 ⟶ 𝐴 ) |
45 |
44
|
frnd |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ran 𝑔 ⊆ 𝐴 ) |
46 |
|
undif |
⊢ ( ran 𝑔 ⊆ 𝐴 ↔ ( ran 𝑔 ∪ ( 𝐴 ∖ ran 𝑔 ) ) = 𝐴 ) |
47 |
45 46
|
sylib |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( ran 𝑔 ∪ ( 𝐴 ∖ ran 𝑔 ) ) = 𝐴 ) |
48 |
43 47
|
eqtrid |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → dom ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐴 ) |
49 |
48
|
adantl |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → dom ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐴 ) |
50 |
|
df-fn |
⊢ ( ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) Fn 𝐴 ↔ ( Fun ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ∧ dom ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐴 ) ) |
51 |
39 49 50
|
sylanbrc |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) Fn 𝐴 ) |
52 |
|
rnun |
⊢ ran ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( ran ◡ 𝑔 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) |
53 |
|
dfdm4 |
⊢ dom 𝑔 = ran ◡ 𝑔 |
54 |
|
f1dm |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → dom 𝑔 = 𝐵 ) |
55 |
53 54
|
eqtr3id |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ran ◡ 𝑔 = 𝐵 ) |
56 |
55
|
uneq1d |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( ran ◡ 𝑔 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = ( 𝐵 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ) |
57 |
|
xpeq1 |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ( ∅ × { 𝑧 } ) ) |
58 |
|
0xp |
⊢ ( ∅ × { 𝑧 } ) = ∅ |
59 |
57 58
|
eqtrdi |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ∅ ) |
60 |
59
|
rneqd |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ran ∅ ) |
61 |
|
rn0 |
⊢ ran ∅ = ∅ |
62 |
60 61
|
eqtrdi |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = ∅ ) |
63 |
|
0ss |
⊢ ∅ ⊆ 𝐵 |
64 |
62 63
|
eqsstrdi |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ) |
65 |
64
|
a1d |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) = ∅ → ( 𝑧 ∈ 𝐵 → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ) ) |
66 |
|
rnxp |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) ≠ ∅ → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = { 𝑧 } ) |
67 |
66
|
adantr |
⊢ ( ( ( 𝐴 ∖ ran 𝑔 ) ≠ ∅ ∧ 𝑧 ∈ 𝐵 ) → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) = { 𝑧 } ) |
68 |
|
snssi |
⊢ ( 𝑧 ∈ 𝐵 → { 𝑧 } ⊆ 𝐵 ) |
69 |
68
|
adantl |
⊢ ( ( ( 𝐴 ∖ ran 𝑔 ) ≠ ∅ ∧ 𝑧 ∈ 𝐵 ) → { 𝑧 } ⊆ 𝐵 ) |
70 |
67 69
|
eqsstrd |
⊢ ( ( ( 𝐴 ∖ ran 𝑔 ) ≠ ∅ ∧ 𝑧 ∈ 𝐵 ) → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ) |
71 |
70
|
ex |
⊢ ( ( 𝐴 ∖ ran 𝑔 ) ≠ ∅ → ( 𝑧 ∈ 𝐵 → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ) ) |
72 |
65 71
|
pm2.61ine |
⊢ ( 𝑧 ∈ 𝐵 → ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ) |
73 |
|
ssequn2 |
⊢ ( ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ⊆ 𝐵 ↔ ( 𝐵 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐵 ) |
74 |
72 73
|
sylib |
⊢ ( 𝑧 ∈ 𝐵 → ( 𝐵 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐵 ) |
75 |
56 74
|
sylan9eqr |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → ( ran ◡ 𝑔 ∪ ran ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐵 ) |
76 |
52 75
|
eqtrid |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → ran ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐵 ) |
77 |
|
df-fo |
⊢ ( ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) : 𝐴 –onto→ 𝐵 ↔ ( ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) Fn 𝐴 ∧ ran ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) = 𝐵 ) ) |
78 |
51 76 77
|
sylanbrc |
⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) : 𝐴 –onto→ 𝐵 ) |
79 |
|
foeq1 |
⊢ ( 𝑓 = ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) → ( 𝑓 : 𝐴 –onto→ 𝐵 ↔ ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) : 𝐴 –onto→ 𝐵 ) ) |
80 |
79
|
spcegv |
⊢ ( ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) ∈ Fin → ( ( ◡ 𝑔 ∪ ( ( 𝐴 ∖ ran 𝑔 ) × { 𝑧 } ) ) : 𝐴 –onto→ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) |
81 |
21 78 80
|
syl2im |
⊢ ( ( 𝑔 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( 𝑧 ∈ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) |
82 |
81
|
expcomd |
⊢ ( ( 𝑔 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
83 |
82
|
com12 |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( ( 𝑔 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
84 |
14 83
|
syland |
⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 → ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
85 |
84
|
exlimiv |
⊢ ( ∃ 𝑔 𝑔 : 𝐵 –1-1→ 𝐴 → ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
86 |
10 85
|
syl |
⊢ ( 𝐵 ≼ 𝐴 → ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
87 |
86
|
adantl |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) ) |
88 |
8 9 87
|
mp2and |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) |
89 |
88
|
exlimdv |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ( ∃ 𝑧 𝑧 ∈ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) |
90 |
7 89
|
syl5 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ( ∅ ≺ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) |
91 |
90
|
3impia |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ ∅ ≺ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) |
92 |
91
|
3com23 |
⊢ ( ( 𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) |