Metamath Proof Explorer

Theorem isf34lem7

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypothesis compss.a 
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem7 
|- ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> U. ran G e. ran G )

Proof

Step Hyp Ref Expression
1 compss.a 
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 1 isf34lem2 
 |-  ( A e. Fin3 -> F : ~P A --> ~P A )
3 2 adantr 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> F : ~P A --> ~P A )
4 3 3adant3 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> F : ~P A --> ~P A )
5 4 ffnd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> F Fn ~P A )
6 imassrn 
 |-  ( F " ran G ) C_ ran F
7 3 frnd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ran F C_ ~P A )
8 7 3adant3 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> ran F C_ ~P A )
9 6 8 sstrid 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> ( F " ran G ) C_ ~P A )
10 simp1 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> A e. Fin3 )
11 fco 
 |-  ( ( F : ~P A --> ~P A /\ G : _om --> ~P A ) -> ( F o. G ) : _om --> ~P A )
12 2 11 sylan 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F o. G ) : _om --> ~P A )
13 12 3adant3 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> ( F o. G ) : _om --> ~P A )
14 sscon 
 |-  ( ( G ` y ) C_ ( G ` suc y ) -> ( A \ ( G ` suc y ) ) C_ ( A \ ( G ` y ) ) )
15 simpr 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> G : _om --> ~P A )
16 peano2 
 |-  ( y e. _om -> suc y e. _om )
17 fvco3 
 |-  ( ( G : _om --> ~P A /\ suc y e. _om ) -> ( ( F o. G ) ` suc y ) = ( F ` ( G ` suc y ) ) )
18 15 16 17 syl2an 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( F o. G ) ` suc y ) = ( F ` ( G ` suc y ) ) )
19 simpll 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> A e. Fin3 )
20 ffvelcdm 
 |-  ( ( G : _om --> ~P A /\ suc y e. _om ) -> ( G ` suc y ) e. ~P A )
21 15 16 20 syl2an 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( G ` suc y ) e. ~P A )
22 21 elpwid 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( G ` suc y ) C_ A )
23 1 isf34lem1 
 |-  ( ( A e. Fin3 /\ ( G ` suc y ) C_ A ) -> ( F ` ( G ` suc y ) ) = ( A \ ( G ` suc y ) ) )
24 19 22 23 syl2anc 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( F ` ( G ` suc y ) ) = ( A \ ( G ` suc y ) ) )
25 18 24 eqtrd 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( F o. G ) ` suc y ) = ( A \ ( G ` suc y ) ) )
26 fvco3 
 |-  ( ( G : _om --> ~P A /\ y e. _om ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
27 26 adantll 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
28 ffvelcdm 
 |-  ( ( G : _om --> ~P A /\ y e. _om ) -> ( G ` y ) e. ~P A )
29 28 adantll 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( G ` y ) e. ~P A )
30 29 elpwid 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( G ` y ) C_ A )
31 1 isf34lem1 
 |-  ( ( A e. Fin3 /\ ( G ` y ) C_ A ) -> ( F ` ( G ` y ) ) = ( A \ ( G ` y ) ) )
32 19 30 31 syl2anc 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( F ` ( G ` y ) ) = ( A \ ( G ` y ) ) )
33 27 32 eqtrd 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( F o. G ) ` y ) = ( A \ ( G ` y ) ) )
34 25 33 sseq12d 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( ( F o. G ) ` suc y ) C_ ( ( F o. G ) ` y ) <-> ( A \ ( G ` suc y ) ) C_ ( A \ ( G ` y ) ) ) )
35 14 34 imbitrrid 
 |-  ( ( ( A e. Fin3 /\ G : _om --> ~P A ) /\ y e. _om ) -> ( ( G ` y ) C_ ( G ` suc y ) -> ( ( F o. G ) ` suc y ) C_ ( ( F o. G ) ` y ) ) )
36 35 ralimdva 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( A. y e. _om ( G ` y ) C_ ( G ` suc y ) -> A. y e. _om ( ( F o. G ) ` suc y ) C_ ( ( F o. G ) ` y ) ) )
37 36 3impia 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> A. y e. _om ( ( F o. G ) ` suc y ) C_ ( ( F o. G ) ` y ) )
38 fin33i 
 |-  ( ( A e. Fin3 /\ ( F o. G ) : _om --> ~P A /\ A. y e. _om ( ( F o. G ) ` suc y ) C_ ( ( F o. G ) ` y ) ) -> |^| ran ( F o. G ) e. ran ( F o. G ) )
39 10 13 37 38 syl3anc 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> |^| ran ( F o. G ) e. ran ( F o. G ) )
40 rnco2 
 |-  ran ( F o. G ) = ( F " ran G )
41 40 inteqi 
 |-  |^| ran ( F o. G ) = |^| ( F " ran G )
42 39 41 40 3eltr3g 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> |^| ( F " ran G ) e. ( F " ran G ) )
43 fnfvima 
 |-  ( ( F Fn ~P A /\ ( F " ran G ) C_ ~P A /\ |^| ( F " ran G ) e. ( F " ran G ) ) -> ( F ` |^| ( F " ran G ) ) e. ( F " ( F " ran G ) ) )
44 5 9 42 43 syl3anc 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> ( F ` |^| ( F " ran G ) ) e. ( F " ( F " ran G ) ) )
45 simpl 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> A e. Fin3 )
46 6 7 sstrid 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F " ran G ) C_ ~P A )
47 incom 
 |-  ( dom F i^i ran G ) = ( ran G i^i dom F )
48 frn 
 |-  ( G : _om --> ~P A -> ran G C_ ~P A )
49 48 adantl 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ran G C_ ~P A )
50 3 fdmd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> dom F = ~P A )
51 49 50 sseqtrrd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ran G C_ dom F )
52 dfss2 
 |-  ( ran G C_ dom F <-> ( ran G i^i dom F ) = ran G )
53 51 52 sylib 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( ran G i^i dom F ) = ran G )
54 47 53 eqtrid 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( dom F i^i ran G ) = ran G )
55 fdm 
 |-  ( G : _om --> ~P A -> dom G = _om )
56 55 adantl 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> dom G = _om )
57 peano1 
 |-  (/) e. _om
58 ne0i 
 |-  ( (/) e. _om -> _om =/= (/) )
59 57 58 mp1i 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> _om =/= (/) )
60 56 59 eqnetrd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> dom G =/= (/) )
61 dm0rn0 
 |-  ( dom G = (/) <-> ran G = (/) )
62 61 necon3bii 
 |-  ( dom G =/= (/) <-> ran G =/= (/) )
63 60 62 sylib 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ran G =/= (/) )
64 54 63 eqnetrd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( dom F i^i ran G ) =/= (/) )
65 imadisj 
 |-  ( ( F " ran G ) = (/) <-> ( dom F i^i ran G ) = (/) )
66 65 necon3bii 
 |-  ( ( F " ran G ) =/= (/) <-> ( dom F i^i ran G ) =/= (/) )
67 64 66 sylibr 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F " ran G ) =/= (/) )
68 1 isf34lem5 
 |-  ( ( A e. Fin3 /\ ( ( F " ran G ) C_ ~P A /\ ( F " ran G ) =/= (/) ) ) -> ( F ` |^| ( F " ran G ) ) = U. ( F " ( F " ran G ) ) )
69 45 46 67 68 syl12anc 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F ` |^| ( F " ran G ) ) = U. ( F " ( F " ran G ) ) )
70 1 isf34lem3 
 |-  ( ( A e. Fin3 /\ ran G C_ ~P A ) -> ( F " ( F " ran G ) ) = ran G )
71 45 49 70 syl2anc 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F " ( F " ran G ) ) = ran G )
72 71 unieqd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> U. ( F " ( F " ran G ) ) = U. ran G )
73 69 72 eqtrd 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( F ` |^| ( F " ran G ) ) = U. ran G )
74 73 71 eleq12d 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A ) -> ( ( F ` |^| ( F " ran G ) ) e. ( F " ( F " ran G ) ) <-> U. ran G e. ran G ) )
75 74 3adant3 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> ( ( F ` |^| ( F " ran G ) ) e. ( F " ( F " ran G ) ) <-> U. ran G e. ran G ) )
76 44 75 mpbid 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. y e. _om ( G ` y ) C_ ( G ` suc y ) ) -> U. ran G e. ran G )