Metamath Proof Explorer

Theorem pwfseqlem3

Description: Lemma for pwfseq . Using the construction D from pwfseqlem1 , produce a function F that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015)

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 pwfseqlem3 
|- ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )

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 vex 
 |-  x e. _V
9 vex 
 |-  r e. _V
10 fvex 
 |-  ( H ` ( card ` x ) ) e. _V
11 fvex 
 |-  ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. _V
12 10 11 ifex 
 |-  if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V
13 7 ovmpt4g 
 |-  ( ( x e. _V /\ r e. _V /\ if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V ) -> ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
14 8 9 12 13 mp3an 
 |-  ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) )
15 4 simprbi 
 |-  ( ps -> _om ~<_ x )
16 15 adantl 
 |-  ( ( ph /\ ps ) -> _om ~<_ x )
17 domnsym 
 |-  ( _om ~<_ x -> -. x ~< _om )
18 16 17 syl 
 |-  ( ( ph /\ ps ) -> -. x ~< _om )
19 isfinite 
 |-  ( x e. Fin <-> x ~< _om )
20 18 19 sylnibr 
 |-  ( ( ph /\ ps ) -> -. x e. Fin )
21 20 iffalsed 
 |-  ( ( ph /\ ps ) -> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) = ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) )
22 14 21 syl5eq 
 |-  ( ( ph /\ ps ) -> ( x F r ) = ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) )
23 1 2 3 4 5 6 pwfseqlem1 
 |-  ( ( ph /\ ps ) -> D e. ( U_ n e. _om ( A ^m n ) \ U_ n e. _om ( x ^m n ) ) )
24 eldif 
 |-  ( D e. ( U_ n e. _om ( A ^m n ) \ U_ n e. _om ( x ^m n ) ) <-> ( D e. U_ n e. _om ( A ^m n ) /\ -. D e. U_ n e. _om ( x ^m n ) ) )
25 23 24 sylib 
 |-  ( ( ph /\ ps ) -> ( D e. U_ n e. _om ( A ^m n ) /\ -. D e. U_ n e. _om ( x ^m n ) ) )
26 25 simpld 
 |-  ( ( ph /\ ps ) -> D e. U_ n e. _om ( A ^m n ) )
27 eliun 
 |-  ( D e. U_ n e. _om ( A ^m n ) <-> E. n e. _om D e. ( A ^m n ) )
28 26 27 sylib 
 |-  ( ( ph /\ ps ) -> E. n e. _om D e. ( A ^m n ) )
29 elmapi 
 |-  ( D e. ( A ^m n ) -> D : n --> A )
30 29 ad2antll 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> D : n --> A )
31 ssiun2 
 |-  ( n e. _om -> ( x ^m n ) C_ U_ n e. _om ( x ^m n ) )
32 31 ad2antrl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( x ^m n ) C_ U_ n e. _om ( x ^m n ) )
33 25 simprd 
 |-  ( ( ph /\ ps ) -> -. D e. U_ n e. _om ( x ^m n ) )
34 33 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> -. D e. U_ n e. _om ( x ^m n ) )
35 32 34 ssneldd 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> -. D e. ( x ^m n ) )
36 vex 
 |-  n e. _V
37 8 36 elmap 
 |-  ( D e. ( x ^m n ) <-> D : n --> x )
38 ffn 
 |-  ( D : n --> A -> D Fn n )
39 ffnfv 
 |-  ( D : n --> x <-> ( D Fn n /\ A. z e. n ( D ` z ) e. x ) )
40 39 baib 
 |-  ( D Fn n -> ( D : n --> x <-> A. z e. n ( D ` z ) e. x ) )
41 30 38 40 3syl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( D : n --> x <-> A. z e. n ( D ` z ) e. x ) )
42 37 41 syl5bb 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( D e. ( x ^m n ) <-> A. z e. n ( D ` z ) e. x ) )
43 35 42 mtbid 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> -. A. z e. n ( D ` z ) e. x )
44 nnon 
 |-  ( n e. _om -> n e. On )
45 44 ad2antrl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> n e. On )
46 ssrab2 
 |-  { z e. _om | -. ( D ` z ) e. x } C_ _om
47 omsson 
 |-  _om C_ On
48 46 47 sstri 
 |-  { z e. _om | -. ( D ` z ) e. x } C_ On
49 ordom 
 |-  Ord _om
50 simprl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> n e. _om )
51 ordelss 
 |-  ( ( Ord _om /\ n e. _om ) -> n C_ _om )
52 49 50 51 sylancr 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> n C_ _om )
53 rexnal 
 |-  ( E. z e. n -. ( D ` z ) e. x <-> -. A. z e. n ( D ` z ) e. x )
54 43 53 sylibr 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> E. z e. n -. ( D ` z ) e. x )
55 ssrexv 
 |-  ( n C_ _om -> ( E. z e. n -. ( D ` z ) e. x -> E. z e. _om -. ( D ` z ) e. x ) )
56 52 54 55 sylc 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> E. z e. _om -. ( D ` z ) e. x )
57 rabn0 
 |-  ( { z e. _om | -. ( D ` z ) e. x } =/= (/) <-> E. z e. _om -. ( D ` z ) e. x )
58 56 57 sylibr 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> { z e. _om | -. ( D ` z ) e. x } =/= (/) )
59 onint 
 |-  ( ( { z e. _om | -. ( D ` z ) e. x } C_ On /\ { z e. _om | -. ( D ` z ) e. x } =/= (/) ) -> |^| { z e. _om | -. ( D ` z ) e. x } e. { z e. _om | -. ( D ` z ) e. x } )
60 48 58 59 sylancr 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> |^| { z e. _om | -. ( D ` z ) e. x } e. { z e. _om | -. ( D ` z ) e. x } )
61 48 60 sseldi 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> |^| { z e. _om | -. ( D ` z ) e. x } e. On )
62 ontri1 
 |-  ( ( n e. On /\ |^| { z e. _om | -. ( D ` z ) e. x } e. On ) -> ( n C_ |^| { z e. _om | -. ( D ` z ) e. x } <-> -. |^| { z e. _om | -. ( D ` z ) e. x } e. n ) )
63 45 61 62 syl2anc 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( n C_ |^| { z e. _om | -. ( D ` z ) e. x } <-> -. |^| { z e. _om | -. ( D ` z ) e. x } e. n ) )
64 ssintrab 
 |-  ( n C_ |^| { z e. _om | -. ( D ` z ) e. x } <-> A. z e. _om ( -. ( D ` z ) e. x -> n C_ z ) )
65 nnon 
 |-  ( z e. _om -> z e. On )
66 ontri1 
 |-  ( ( n e. On /\ z e. On ) -> ( n C_ z <-> -. z e. n ) )
67 44 65 66 syl2an 
 |-  ( ( n e. _om /\ z e. _om ) -> ( n C_ z <-> -. z e. n ) )
68 67 imbi2d 
 |-  ( ( n e. _om /\ z e. _om ) -> ( ( -. ( D ` z ) e. x -> n C_ z ) <-> ( -. ( D ` z ) e. x -> -. z e. n ) ) )
69 con34b 
 |-  ( ( z e. n -> ( D ` z ) e. x ) <-> ( -. ( D ` z ) e. x -> -. z e. n ) )
70 68 69 bitr4di 
 |-  ( ( n e. _om /\ z e. _om ) -> ( ( -. ( D ` z ) e. x -> n C_ z ) <-> ( z e. n -> ( D ` z ) e. x ) ) )
71 70 pm5.74da 
 |-  ( n e. _om -> ( ( z e. _om -> ( -. ( D ` z ) e. x -> n C_ z ) ) <-> ( z e. _om -> ( z e. n -> ( D ` z ) e. x ) ) ) )
72 bi2.04 
 |-  ( ( z e. _om -> ( z e. n -> ( D ` z ) e. x ) ) <-> ( z e. n -> ( z e. _om -> ( D ` z ) e. x ) ) )
73 71 72 bitrdi 
 |-  ( n e. _om -> ( ( z e. _om -> ( -. ( D ` z ) e. x -> n C_ z ) ) <-> ( z e. n -> ( z e. _om -> ( D ` z ) e. x ) ) ) )
74 elnn 
 |-  ( ( z e. n /\ n e. _om ) -> z e. _om )
75 pm2.27 
 |-  ( z e. _om -> ( ( z e. _om -> ( D ` z ) e. x ) -> ( D ` z ) e. x ) )
76 74 75 syl 
 |-  ( ( z e. n /\ n e. _om ) -> ( ( z e. _om -> ( D ` z ) e. x ) -> ( D ` z ) e. x ) )
77 76 expcom 
 |-  ( n e. _om -> ( z e. n -> ( ( z e. _om -> ( D ` z ) e. x ) -> ( D ` z ) e. x ) ) )
78 77 a2d 
 |-  ( n e. _om -> ( ( z e. n -> ( z e. _om -> ( D ` z ) e. x ) ) -> ( z e. n -> ( D ` z ) e. x ) ) )
79 73 78 sylbid 
 |-  ( n e. _om -> ( ( z e. _om -> ( -. ( D ` z ) e. x -> n C_ z ) ) -> ( z e. n -> ( D ` z ) e. x ) ) )
80 79 ad2antrl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( ( z e. _om -> ( -. ( D ` z ) e. x -> n C_ z ) ) -> ( z e. n -> ( D ` z ) e. x ) ) )
81 80 ralimdv2 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( A. z e. _om ( -. ( D ` z ) e. x -> n C_ z ) -> A. z e. n ( D ` z ) e. x ) )
82 64 81 syl5bi 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( n C_ |^| { z e. _om | -. ( D ` z ) e. x } -> A. z e. n ( D ` z ) e. x ) )
83 63 82 sylbird 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( -. |^| { z e. _om | -. ( D ` z ) e. x } e. n -> A. z e. n ( D ` z ) e. x ) )
84 43 83 mt3d 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> |^| { z e. _om | -. ( D ` z ) e. x } e. n )
85 30 84 ffvelrnd 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. A )
86 fveq2 
 |-  ( y = |^| { z e. _om | -. ( D ` z ) e. x } -> ( D ` y ) = ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) )
87 86 eleq1d 
 |-  ( y = |^| { z e. _om | -. ( D ` z ) e. x } -> ( ( D ` y ) e. x <-> ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. x ) )
88 87 notbid 
 |-  ( y = |^| { z e. _om | -. ( D ` z ) e. x } -> ( -. ( D ` y ) e. x <-> -. ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. x ) )
89 fveq2 
 |-  ( z = y -> ( D ` z ) = ( D ` y ) )
90 89 eleq1d 
 |-  ( z = y -> ( ( D ` z ) e. x <-> ( D ` y ) e. x ) )
91 90 notbid 
 |-  ( z = y -> ( -. ( D ` z ) e. x <-> -. ( D ` y ) e. x ) )
92 91 cbvrabv 
 |-  { z e. _om | -. ( D ` z ) e. x } = { y e. _om | -. ( D ` y ) e. x }
93 88 92 elrab2 
 |-  ( |^| { z e. _om | -. ( D ` z ) e. x } e. { z e. _om | -. ( D ` z ) e. x } <-> ( |^| { z e. _om | -. ( D ` z ) e. x } e. _om /\ -. ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. x ) )
94 93 simprbi 
 |-  ( |^| { z e. _om | -. ( D ` z ) e. x } e. { z e. _om | -. ( D ` z ) e. x } -> -. ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. x )
95 60 94 syl 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> -. ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. x )
96 85 95 eldifd 
 |-  ( ( ( ph /\ ps ) /\ ( n e. _om /\ D e. ( A ^m n ) ) ) -> ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. ( A \ x ) )
97 28 96 rexlimddv 
 |-  ( ( ph /\ ps ) -> ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. ( A \ x ) )
98 22 97 eqeltrd 
 |-  ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )