Metamath Proof Explorer

Theorem pwfseqlem1

Description: Lemma for pwfseq . Derive a contradiction by diagonalization. (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 ) ) ) } )
Assertion pwfseqlem1 
|- ( ( ph /\ ps ) -> D e. ( U_ n e. _om ( A ^m n ) \ U_ n e. _om ( x ^m n ) ) )

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 1 adantr 
 |-  ( ( ph /\ ps ) -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
8 f1f 
 |-  ( G : ~P A -1-1-> U_ n e. _om ( A ^m n ) -> G : ~P A --> U_ n e. _om ( A ^m n ) )
9 7 8 syl 
 |-  ( ( ph /\ ps ) -> G : ~P A --> U_ n e. _om ( A ^m n ) )
10 ssrab2 
 |-  { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } C_ x
11 simprl1 
 |-  ( ( ph /\ ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) ) -> x C_ A )
12 4 11 sylan2b 
 |-  ( ( ph /\ ps ) -> x C_ A )
13 10 12 sstrid 
 |-  ( ( ph /\ ps ) -> { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } C_ A )
14 vex 
 |-  x e. _V
15 14 rabex 
 |-  { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. _V
16 15 elpw 
 |-  ( { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. ~P A <-> { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } C_ A )
17 13 16 sylibr 
 |-  ( ( ph /\ ps ) -> { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. ~P A )
18 9 17 ffvelrnd 
 |-  ( ( ph /\ ps ) -> ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) e. U_ n e. _om ( A ^m n ) )
19 6 18 eqeltrid 
 |-  ( ( ph /\ ps ) -> D e. U_ n e. _om ( A ^m n ) )
20 pm5.19 
 |-  -. ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> -. ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
21 5 adantr 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
22 f1f 
 |-  ( K : U_ n e. _om ( x ^m n ) -1-1-> x -> K : U_ n e. _om ( x ^m n ) --> x )
23 21 22 syl 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> K : U_ n e. _om ( x ^m n ) --> x )
24 ffvelrn 
 |-  ( ( K : U_ n e. _om ( x ^m n ) --> x /\ D e. U_ n e. _om ( x ^m n ) ) -> ( K ` D ) e. x )
25 23 24 sylancom 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( K ` D ) e. x )
26 f1f1orn 
 |-  ( K : U_ n e. _om ( x ^m n ) -1-1-> x -> K : U_ n e. _om ( x ^m n ) -1-1-onto-> ran K )
27 21 26 syl 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> K : U_ n e. _om ( x ^m n ) -1-1-onto-> ran K )
28 f1ocnvfv1 
 |-  ( ( K : U_ n e. _om ( x ^m n ) -1-1-onto-> ran K /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) = D )
29 27 28 sylancom 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) = D )
30 f1fn 
 |-  ( G : ~P A -1-1-> U_ n e. _om ( A ^m n ) -> G Fn ~P A )
31 7 30 syl 
 |-  ( ( ph /\ ps ) -> G Fn ~P A )
32 fnfvelrn 
 |-  ( ( G Fn ~P A /\ { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. ~P A ) -> ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) e. ran G )
33 31 17 32 syl2anc 
 |-  ( ( ph /\ ps ) -> ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) e. ran G )
34 6 33 eqeltrid 
 |-  ( ( ph /\ ps ) -> D e. ran G )
35 34 adantr 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> D e. ran G )
36 29 35 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) e. ran G )
37 fveq2 
 |-  ( y = ( K ` D ) -> ( `' K ` y ) = ( `' K ` ( K ` D ) ) )
38 37 eleq1d 
 |-  ( y = ( K ` D ) -> ( ( `' K ` y ) e. ran G <-> ( `' K ` ( K ` D ) ) e. ran G ) )
39 id 
 |-  ( y = ( K ` D ) -> y = ( K ` D ) )
40 2fveq3 
 |-  ( y = ( K ` D ) -> ( `' G ` ( `' K ` y ) ) = ( `' G ` ( `' K ` ( K ` D ) ) ) )
41 39 40 eleq12d 
 |-  ( y = ( K ` D ) -> ( y e. ( `' G ` ( `' K ` y ) ) <-> ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
42 41 notbid 
 |-  ( y = ( K ` D ) -> ( -. y e. ( `' G ` ( `' K ` y ) ) <-> -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
43 38 42 anbi12d 
 |-  ( y = ( K ` D ) -> ( ( ( `' K ` y ) e. ran G /\ -. y e. ( `' G ` ( `' K ` y ) ) ) <-> ( ( `' K ` ( K ` D ) ) e. ran G /\ -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) ) )
44 fveq2 
 |-  ( w = y -> ( `' K ` w ) = ( `' K ` y ) )
45 44 eleq1d 
 |-  ( w = y -> ( ( `' K ` w ) e. ran G <-> ( `' K ` y ) e. ran G ) )
46 id 
 |-  ( w = y -> w = y )
47 2fveq3 
 |-  ( w = y -> ( `' G ` ( `' K ` w ) ) = ( `' G ` ( `' K ` y ) ) )
48 46 47 eleq12d 
 |-  ( w = y -> ( w e. ( `' G ` ( `' K ` w ) ) <-> y e. ( `' G ` ( `' K ` y ) ) ) )
49 48 notbid 
 |-  ( w = y -> ( -. w e. ( `' G ` ( `' K ` w ) ) <-> -. y e. ( `' G ` ( `' K ` y ) ) ) )
50 45 49 anbi12d 
 |-  ( w = y -> ( ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) <-> ( ( `' K ` y ) e. ran G /\ -. y e. ( `' G ` ( `' K ` y ) ) ) ) )
51 50 cbvrabv 
 |-  { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } = { y e. x | ( ( `' K ` y ) e. ran G /\ -. y e. ( `' G ` ( `' K ` y ) ) ) }
52 43 51 elrab2 
 |-  ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> ( ( K ` D ) e. x /\ ( ( `' K ` ( K ` D ) ) e. ran G /\ -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) ) )
53 anass 
 |-  ( ( ( ( K ` D ) e. x /\ ( `' K ` ( K ` D ) ) e. ran G ) /\ -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) <-> ( ( K ` D ) e. x /\ ( ( `' K ` ( K ` D ) ) e. ran G /\ -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) ) )
54 52 53 bitr4i 
 |-  ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> ( ( ( K ` D ) e. x /\ ( `' K ` ( K ` D ) ) e. ran G ) /\ -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
55 54 baib 
 |-  ( ( ( K ` D ) e. x /\ ( `' K ` ( K ` D ) ) e. ran G ) -> ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
56 25 36 55 syl2anc 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
57 29 6 eqtrdi 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) )
58 57 fveq2d 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' G ` ( `' K ` ( K ` D ) ) ) = ( `' G ` ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) ) )
59 f1f1orn 
 |-  ( G : ~P A -1-1-> U_ n e. _om ( A ^m n ) -> G : ~P A -1-1-onto-> ran G )
60 7 59 syl 
 |-  ( ( ph /\ ps ) -> G : ~P A -1-1-onto-> ran G )
61 f1ocnvfv1 
 |-  ( ( G : ~P A -1-1-onto-> ran G /\ { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. ~P A ) -> ( `' G ` ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) ) = { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
62 60 17 61 syl2anc 
 |-  ( ( ph /\ ps ) -> ( `' G ` ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) ) = { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
63 62 adantr 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' G ` ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) ) = { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
64 58 63 eqtrd 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( `' G ` ( `' K ` ( K ` D ) ) ) = { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
65 64 eleq2d 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) <-> ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) )
66 65 notbid 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) <-> -. ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) )
67 56 66 bitrd 
 |-  ( ( ( ph /\ ps ) /\ D e. U_ n e. _om ( x ^m n ) ) -> ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> -. ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) )
68 67 ex 
 |-  ( ( ph /\ ps ) -> ( D e. U_ n e. _om ( x ^m n ) -> ( ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } <-> -. ( K ` D ) e. { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) ) )
69 20 68 mtoi 
 |-  ( ( ph /\ ps ) -> -. D e. U_ n e. _om ( x ^m n ) )
70 19 69 eldifd 
 |-  ( ( ph /\ ps ) -> D e. ( U_ n e. _om ( A ^m n ) \ U_ n e. _om ( x ^m n ) ) )