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 
|- ( ( ( F e. V /\ A e. W /\ M e. On ) /\ F : A -1-1-onto-> suc M ) -> ( A \ { ( `' F ` M ) } ) ~~ M )

Proof

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