Metamath Proof Explorer

Theorem dif1enlem

Description: Lemma for rexdif1en and dif1en . (Contributed by BTernaryTau, 18-Aug-2024) Generalize to all ordinals and add a sethood requirement to avoid ax-un . (Revised by BTernaryTau, 5-Jan-2025)

Ref Expression
Assertion dif1enlem ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On ) ∧ 𝐹 : 𝐴 –1-1-onto→ suc 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 )

Proof

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 𝑀 ) → ( 𝐴 ∖ { ( ◡ 𝐹 ‘ 𝑀 ) } ) ≈ 𝑀 )