Metamath Proof Explorer

Theorem dif1enlem

Description: Lemma for rexdif1en and dif1en . (Contributed by BTernaryTau, 18-Aug-2024)

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

Proof

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