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