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 ffvelrn
 |-  ( ( 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 syl5bir
 |-  ( ( 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 syl5bb
 |-  ( 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 )