Step |
Hyp |
Ref |
Expression |
1 |
|
sucidg |
⊢ ( 𝑀 ∈ On → 𝑀 ∈ suc 𝑀 ) |
2 |
|
dff1o3 |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ↔ ( 𝐹 : 𝐴 –onto→ suc 𝑀 ∧ Fun ◡ 𝐹 ) ) |
3 |
2
|
simprbi |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → Fun ◡ 𝐹 ) |
4 |
3
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → Fun ◡ 𝐹 ) |
5 |
|
f1ofo |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → 𝐹 : 𝐴 –onto→ suc 𝑀 ) |
6 |
|
f1ofn |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → 𝐹 Fn 𝐴 ) |
7 |
|
fnresdm |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
8 |
|
foeq1 |
⊢ ( ( 𝐹 ↾ 𝐴 ) = 𝐹 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ suc 𝑀 ↔ 𝐹 : 𝐴 –onto→ suc 𝑀 ) ) |
9 |
6 7 8
|
3syl |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ suc 𝑀 ↔ 𝐹 : 𝐴 –onto→ suc 𝑀 ) ) |
10 |
5 9
|
mpbird |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ suc 𝑀 ) |
11 |
10
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ suc 𝑀 ) |
12 |
6
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → 𝐹 Fn 𝐴 ) |
13 |
|
f1ocnvdm |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ◡ 𝐹 ‘ 𝑀 ) ∈ 𝐴 ) |
14 |
|
f1ocnvfv2 |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑀 ) ) = 𝑀 ) |
15 |
|
snidg |
⊢ ( 𝑀 ∈ suc 𝑀 → 𝑀 ∈ { 𝑀 } ) |
16 |
15
|
adantl |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → 𝑀 ∈ { 𝑀 } ) |
17 |
14 16
|
eqeltrd |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑀 ) ) ∈ { 𝑀 } ) |
18 |
|
fressnfv |
⊢ ( ( 𝐹 Fn 𝐴 ∧ ( ◡ 𝐹 ‘ 𝑀 ) ∈ 𝐴 ) → ( ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } ⟶ { 𝑀 } ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑀 ) ) ∈ { 𝑀 } ) ) |
19 |
18
|
biimp3ar |
⊢ ( ( 𝐹 Fn 𝐴 ∧ ( ◡ 𝐹 ‘ 𝑀 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑀 ) ) ∈ { 𝑀 } ) → ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } ⟶ { 𝑀 } ) |
20 |
12 13 17 19
|
syl3anc |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } ⟶ { 𝑀 } ) |
21 |
|
disjsn |
⊢ ( ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ↔ ¬ ( ◡ 𝐹 ‘ 𝑀 ) ∈ 𝐴 ) |
22 |
21
|
con2bii |
⊢ ( ( ◡ 𝐹 ‘ 𝑀 ) ∈ 𝐴 ↔ ¬ ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) |
23 |
13 22
|
sylib |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ¬ ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) |
24 |
|
fnresdisj |
⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ↔ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) ) |
25 |
6 24
|
syl |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 → ( ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ↔ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( ( 𝐴 ∩ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ↔ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) ) |
27 |
23 26
|
mtbid |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ¬ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) = ∅ ) |
28 |
27
|
neqned |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≠ ∅ ) |
29 |
|
foconst |
⊢ ( ( ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } ⟶ { 𝑀 } ∧ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≠ ∅ ) → ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } –onto→ { 𝑀 } ) |
30 |
20 28 29
|
syl2anc |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } –onto→ { 𝑀 } ) |
31 |
|
resdif |
⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ suc 𝑀 ∧ ( 𝐹 ↾ { ( ◡ 𝐹 ‘ 𝑀 ) } ) : { ( ◡ 𝐹 ‘ 𝑀 ) } –onto→ { 𝑀 } ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ ( suc 𝑀 ∖ { 𝑀 } ) ) |
32 |
4 11 30 31
|
syl3anc |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ suc 𝑀 ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ ( suc 𝑀 ∖ { 𝑀 } ) ) |
33 |
1 32
|
sylan2 |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ On ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ ( suc 𝑀 ∖ { 𝑀 } ) ) |
34 |
|
eloni |
⊢ ( 𝑀 ∈ On → Ord 𝑀 ) |
35 |
|
orddif |
⊢ ( Ord 𝑀 → 𝑀 = ( suc 𝑀 ∖ { 𝑀 } ) ) |
36 |
34 35
|
syl |
⊢ ( 𝑀 ∈ On → 𝑀 = ( suc 𝑀 ∖ { 𝑀 } ) ) |
37 |
36
|
f1oeq3d |
⊢ ( 𝑀 ∈ On → ( ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ↔ ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ ( suc 𝑀 ∖ { 𝑀 } ) ) ) |
38 |
37
|
adantl |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ On ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ↔ ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ ( suc 𝑀 ∖ { 𝑀 } ) ) ) |
39 |
33 38
|
mpbird |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ∧ 𝑀 ∈ On ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) |
40 |
39
|
ancoms |
⊢ ( ( 𝑀 ∈ On ∧ 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) |
41 |
40
|
3ad2antl3 |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On ) ∧ 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) |
42 |
|
difexg |
⊢ ( 𝐴 ∈ 𝑊 → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ∈ V ) |
43 |
|
resexg |
⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) ∈ V ) |
44 |
|
f1oen4g |
⊢ ( ( ( ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) ∈ V ∧ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ∈ V ∧ 𝑀 ∈ On ) ∧ ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 ) |
45 |
43 44
|
syl3anl1 |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ∈ V ∧ 𝑀 ∈ On ) ∧ ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 ) |
46 |
42 45
|
syl3anl2 |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On ) ∧ ( 𝐹 ↾ ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ) : ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) –1-1-onto→ 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 ) |
47 |
41 46
|
syldan |
⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On ) ∧ 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 ) |