Metamath Proof Explorer

Theorem dif1enlem

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

Ref Expression
Assertion dif1enlem 
|- ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> ( A \ { ( `' F ` M ) } ) ~~ M )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> F e. V )
2 sucidg 
 |-  ( M e. _om -> M e. suc M )
3 dff1o3 
 |-  ( F : A -1-1-onto-> suc M <-> ( F : A -onto-> suc M /\ Fun `' F ) )
4 3 simprbi 
 |-  ( F : A -1-1-onto-> suc M -> Fun `' F )
5 4 adantr 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> Fun `' F )
6 f1ofo 
 |-  ( F : A -1-1-onto-> suc M -> F : A -onto-> suc M )
7 f1ofn 
 |-  ( F : A -1-1-onto-> suc M -> F Fn A )
8 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
9 foeq1 
 |-  ( ( F |` A ) = F -> ( ( F |` A ) : A -onto-> suc M <-> F : A -onto-> suc M ) )
10 7 8 9 3syl 
 |-  ( F : A -1-1-onto-> suc M -> ( ( F |` A ) : A -onto-> suc M <-> F : A -onto-> suc M ) )
11 6 10 mpbird 
 |-  ( F : A -1-1-onto-> suc M -> ( F |` A ) : A -onto-> suc M )
12 11 adantr 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F |` A ) : A -onto-> suc M )
13 7 adantr 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> F Fn A )
14 f1ocnvdm 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' F ` M ) e. A )
15 f1ocnvfv2 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F ` ( `' F ` M ) ) = M )
16 snidg 
 |-  ( M e. suc M -> M e. { M } )
17 16 adantl 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> M e. { M } )
18 15 17 eqeltrd 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F ` ( `' F ` M ) ) e. { M } )
19 fressnfv 
 |-  ( ( F Fn A /\ ( `' F ` M ) e. A ) -> ( ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } --> { M } <-> ( F ` ( `' F ` M ) ) e. { M } ) )
20 19 biimp3ar 
 |-  ( ( F Fn A /\ ( `' F ` M ) e. A /\ ( F ` ( `' F ` M ) ) e. { M } ) -> ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } --> { M } )
21 13 14 18 20 syl3anc 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } --> { M } )
22 disjsn 
 |-  ( ( A i^i { ( `' F ` M ) } ) = (/) <-> -. ( `' F ` M ) e. A )
23 22 con2bii 
 |-  ( ( `' F ` M ) e. A <-> -. ( A i^i { ( `' F ` M ) } ) = (/) )
24 14 23 sylib 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> -. ( A i^i { ( `' F ` M ) } ) = (/) )
25 fnresdisj 
 |-  ( F Fn A -> ( ( A i^i { ( `' F ` M ) } ) = (/) <-> ( F |` { ( `' F ` M ) } ) = (/) ) )
26 7 25 syl 
 |-  ( F : A -1-1-onto-> suc M -> ( ( A i^i { ( `' F ` M ) } ) = (/) <-> ( F |` { ( `' F ` M ) } ) = (/) ) )
27 26 adantr 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( ( A i^i { ( `' F ` M ) } ) = (/) <-> ( F |` { ( `' F ` M ) } ) = (/) ) )
28 24 27 mtbid 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> -. ( F |` { ( `' F ` M ) } ) = (/) )
29 28 neqned 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F |` { ( `' F ` M ) } ) =/= (/) )
30 foconst 
 |-  ( ( ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } --> { M } /\ ( F |` { ( `' F ` M ) } ) =/= (/) ) -> ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } -onto-> { M } )
31 21 29 30 syl2anc 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } -onto-> { M } )
32 resdif 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> suc M /\ ( F |` { ( `' F ` M ) } ) : { ( `' F ` M ) } -onto-> { M } ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> ( suc M \ { M } ) )
33 5 12 31 32 syl3anc 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. suc M ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> ( suc M \ { M } ) )
34 2 33 sylan2 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. _om ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> ( suc M \ { M } ) )
35 nnord 
 |-  ( M e. _om -> Ord M )
36 orddif 
 |-  ( Ord M -> M = ( suc M \ { M } ) )
37 35 36 syl 
 |-  ( M e. _om -> M = ( suc M \ { M } ) )
38 37 f1oeq3d 
 |-  ( M e. _om -> ( ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M <-> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> ( suc M \ { M } ) ) )
39 38 adantl 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. _om ) -> ( ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M <-> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> ( suc M \ { M } ) ) )
40 34 39 mpbird 
 |-  ( ( F : A -1-1-onto-> suc M /\ M e. _om ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M )
41 40 ancoms 
 |-  ( ( M e. _om /\ F : A -1-1-onto-> suc M ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M )
42 41 3adant1 
 |-  ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M )
43 resexg 
 |-  ( F e. V -> ( F |` ( A \ { ( `' F ` M ) } ) ) e. _V )
44 f1oen3g 
 |-  ( ( ( F |` ( A \ { ( `' F ` M ) } ) ) e. _V /\ ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M ) -> ( A \ { ( `' F ` M ) } ) ~~ M )
45 43 44 sylan 
 |-  ( ( F e. V /\ ( F |` ( A \ { ( `' F ` M ) } ) ) : ( A \ { ( `' F ` M ) } ) -1-1-onto-> M ) -> ( A \ { ( `' F ` M ) } ) ~~ M )
46 1 42 45 syl2anc 
 |-  ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> ( A \ { ( `' F ` M ) } ) ~~ M )