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 eqtrid
 |-  ( ( 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 sselid
 |-  ( ( ( 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 ) )