Metamath Proof Explorer

Theorem pwfseqlem4a

Description: Lemma for pwfseqlem4 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pwfseqlem4.g 
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
pwfseqlem4.x 
|- ( ph -> X C_ A )
pwfseqlem4.h 
|- ( ph -> H : _om -1-1-onto-> X )
pwfseqlem4.ps 
|- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
pwfseqlem4.k 
|- ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
pwfseqlem4.d 
|- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
pwfseqlem4.f 
|- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
Assertion pwfseqlem4a 
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A )

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g 
 |-  ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
2 pwfseqlem4.x 
 |-  ( ph -> X C_ A )
3 pwfseqlem4.h 
 |-  ( ph -> H : _om -1-1-onto-> X )
4 pwfseqlem4.ps 
 |-  ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
5 pwfseqlem4.k 
 |-  ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
6 pwfseqlem4.d 
 |-  D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
7 pwfseqlem4.f 
 |-  F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
8 isfinite 
 |-  ( a e. Fin <-> a ~< _om )
9 simpr 
 |-  ( ( ph /\ a e. Fin ) -> a e. Fin )
10 vex 
 |-  s e. _V
11 1 2 3 4 5 6 7 pwfseqlem2 
 |-  ( ( a e. Fin /\ s e. _V ) -> ( a F s ) = ( H ` ( card ` a ) ) )
12 9 10 11 sylancl 
 |-  ( ( ph /\ a e. Fin ) -> ( a F s ) = ( H ` ( card ` a ) ) )
13 f1of 
 |-  ( H : _om -1-1-onto-> X -> H : _om --> X )
14 3 13 syl 
 |-  ( ph -> H : _om --> X )
15 14 2 fssd 
 |-  ( ph -> H : _om --> A )
16 ficardom 
 |-  ( a e. Fin -> ( card ` a ) e. _om )
17 ffvelcdm 
 |-  ( ( H : _om --> A /\ ( card ` a ) e. _om ) -> ( H ` ( card ` a ) ) e. A )
18 15 16 17 syl2an 
 |-  ( ( ph /\ a e. Fin ) -> ( H ` ( card ` a ) ) e. A )
19 12 18 eqeltrd 
 |-  ( ( ph /\ a e. Fin ) -> ( a F s ) e. A )
20 19 ex 
 |-  ( ph -> ( a e. Fin -> ( a F s ) e. A ) )
21 20 adantr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a e. Fin -> ( a F s ) e. A ) )
22 8 21 biimtrrid 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a ~< _om -> ( a F s ) e. A ) )
23 omelon 
 |-  _om e. On
24 onenon 
 |-  ( _om e. On -> _om e. dom card )
25 23 24 ax-mp 
 |-  _om e. dom card
26 simpr3 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> s We a )
27 26 19.8ad 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> E. s s We a )
28 ween 
 |-  ( a e. dom card <-> E. s s We a )
29 27 28 sylibr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> a e. dom card )
30 domtri2 
 |-  ( ( _om e. dom card /\ a e. dom card ) -> ( _om ~<_ a <-> -. a ~< _om ) )
31 25 29 30 sylancr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a <-> -. a ~< _om ) )
32 nfv 
 |-  F/ r ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) )
33 nfcv 
 |-  F/_ r a
34 nfmpo2 
 |-  F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
35 7 34 nfcxfr 
 |-  F/_ r F
36 nfcv 
 |-  F/_ r s
37 33 35 36 nfov 
 |-  F/_ r ( a F s )
38 37 nfel1 
 |-  F/ r ( a F s ) e. ( A \ a )
39 32 38 nfim 
 |-  F/ r ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
40 sseq1 
 |-  ( r = s -> ( r C_ ( a X. a ) <-> s C_ ( a X. a ) ) )
41 weeq1 
 |-  ( r = s -> ( r We a <-> s We a ) )
42 40 41 3anbi23d 
 |-  ( r = s -> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) <-> ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) )
43 42 anbi1d 
 |-  ( r = s -> ( ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) <-> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) )
44 43 anbi2d 
 |-  ( r = s -> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) <-> ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) ) )
45 oveq2 
 |-  ( r = s -> ( a F r ) = ( a F s ) )
46 45 eleq1d 
 |-  ( r = s -> ( ( a F r ) e. ( A \ a ) <-> ( a F s ) e. ( A \ a ) ) )
47 44 46 imbi12d 
 |-  ( r = s -> ( ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) <-> ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) ) ) )
48 nfv 
 |-  F/ x ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) )
49 nfcv 
 |-  F/_ x a
50 nfmpo1 
 |-  F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
51 7 50 nfcxfr 
 |-  F/_ x F
52 nfcv 
 |-  F/_ x r
53 49 51 52 nfov 
 |-  F/_ x ( a F r )
54 53 nfel1 
 |-  F/ x ( a F r ) e. ( A \ a )
55 48 54 nfim 
 |-  F/ x ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
56 sseq1 
 |-  ( x = a -> ( x C_ A <-> a C_ A ) )
57 xpeq12 
 |-  ( ( x = a /\ x = a ) -> ( x X. x ) = ( a X. a ) )
58 57 anidms 
 |-  ( x = a -> ( x X. x ) = ( a X. a ) )
59 58 sseq2d 
 |-  ( x = a -> ( r C_ ( x X. x ) <-> r C_ ( a X. a ) ) )
60 weeq2 
 |-  ( x = a -> ( r We x <-> r We a ) )
61 56 59 60 3anbi123d 
 |-  ( x = a -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) ) )
62 breq2 
 |-  ( x = a -> ( _om ~<_ x <-> _om ~<_ a ) )
63 61 62 anbi12d 
 |-  ( x = a -> ( ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
64 4 63 bitrid 
 |-  ( x = a -> ( ps <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
65 64 anbi2d 
 |-  ( x = a -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) )
66 oveq1 
 |-  ( x = a -> ( x F r ) = ( a F r ) )
67 difeq2 
 |-  ( x = a -> ( A \ x ) = ( A \ a ) )
68 66 67 eleq12d 
 |-  ( x = a -> ( ( x F r ) e. ( A \ x ) <-> ( a F r ) e. ( A \ a ) ) )
69 65 68 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) ) <-> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) ) )
70 1 2 3 4 5 6 7 pwfseqlem3 
 |-  ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )
71 55 69 70 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
72 39 47 71 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
73 72 eldifad 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. A )
74 73 expr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a -> ( a F s ) e. A ) )
75 31 74 sylbird 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( -. a ~< _om -> ( a F s ) e. A ) )
76 22 75 pm2.61d 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A )