Theorem pwfseqlem1 9480

Description: Lemma for pwfseq 9486. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.)

Hypotheses

Ref	Expression
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

Ref	Expression
pwfseqlem1	|- ( ( ph /\ ps ) -> D e. ( U_ n e. om ( A ^m n ) \ U_ n e. om ( x ^m n ) ) )

Distinct variable groups:   n, r, w, x   D, n   w, G   w, K   H, r, x   ph, n, r, x   ps, n   A, n, r, x

Allowed substitution hints:   ph( w)   ps( x, w, r)   A( w)   D( x, w, r)   G( x, n, r)   H( w, n)   K( x, n, r)   X( x, w, n, r)

Proof of Theorem pwfseqlem1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pwfseqlem4.d	. . 3 |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
2		pwfseqlem4.g	. . . . . 6 |- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )
3	2	adantr 481	. . . . 5 |- ( ( ph /\ ps ) -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )
4		f1f 6101	. . . . 5 |- ( G : ~P A -1-1-> U_ n e. om ( A ^m n ) -> G : ~P A --> U_ n e. om ( A ^m n ) )
5	3, 4	syl 17	. . . 4 |- ( ( ph /\ ps ) -> G : ~P A --> U_ n e. om ( A ^m n ) )
6		ssrab2 3687	. . . . . 6 |- { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } C_ x
7		pwfseqlem4.ps	. . . . . . 7 |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )
8		simprl1 1106	. . . . . . 7 |- ( ( ph /\ ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) ) -> x C_ A )
9	7, 8	sylan2b 492	. . . . . 6 |- ( ( ph /\ ps ) -> x C_ A )
10	6, 9	syl5ss 3614	. . . . 5 |- ( ( ph /\ ps ) -> { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } C_ A )
11		vex 3203	. . . . . . 7 |- x e. _V
12	11	rabex 4813	. . . . . 6 |- { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. _V
13	12	elpw 4164	. . . . 5 |- ( { 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 )
14	10, 13	sylibr 224	. . . 4 |- ( ( ph /\ ps ) -> { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } e. ~P A )
15	5, 14	ffvelrnd 6360	. . 3 |- ( ( ph /\ ps ) -> ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) e. U_ n e. om ( A ^m n ) )
16	1, 15	syl5eqel 2705	. 2 |- ( ( ph /\ ps ) -> D e. U_ n e. om ( A ^m n ) )
17		pm5.19 375	. . 3 |- -. ( ( 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 ) ) ) } )
18		pwfseqlem4.k	. . . . . . . . 9 |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )
19	18	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )
20		f1f 6101	. . . . . . . 8 |- ( K : U_ n e. om ( x ^m n ) -1-1-> x -> K : U_ n e. om ( x ^m n ) --> x )
21	19, 20	syl 17	. . . . . . 7 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> K : U_ n e. om ( x ^m n ) --> x )
22		ffvelrn 6357	. . . . . . 7 |- ( ( K : U_ n e. om ( x ^m n ) --> x /\ D e. U_ n e. om ( x ^m n ) ) -> ( K ` D ) e. x )
23	21, 22	sylancom 701	. . . . . 6 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> ( K ` D ) e. x )
24		f1f1orn 6148	. . . . . . . . 9 |- ( K : U_ n e. om ( x ^m n ) -1-1-> x -> K : U_ n e. om ( x ^m n ) -1-1-onto-> ran K )
25	19, 24	syl 17	. . . . . . . 8 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> K : U_ n e. om ( x ^m n ) -1-1-onto-> ran K )
26		f1ocnvfv1 6532	. . . . . . . 8 |- ( ( 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 )
27	25, 26	sylancom 701	. . . . . . 7 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) = D )
28		f1fn 6102	. . . . . . . . . . 11 |- ( G : ~P A -1-1-> U_ n e. om ( A ^m n ) -> G Fn ~P A )
29	3, 28	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ps ) -> G Fn ~P A )
30		fnfvelrn 6356	. . . . . . . . . 10 |- ( ( 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 )
31	29, 14, 30	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ ps ) -> ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) e. ran G )
32	1, 31	syl5eqel 2705	. . . . . . . 8 |- ( ( ph /\ ps ) -> D e. ran G )
33	32	adantr 481	. . . . . . 7 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> D e. ran G )
34	27, 33	eqeltrd 2701	. . . . . 6 |- ( ( ( ph /\ ps ) /\ D e. U_ n e. om ( x ^m n ) ) -> ( `' K ` ( K ` D ) ) e. ran G )
35		fveq2 6191	. . . . . . . . . . 11 |- ( y = ( K ` D ) -> ( `' K ` y ) = ( `' K ` ( K ` D ) ) )
36	35	eleq1d 2686	. . . . . . . . . 10 |- ( y = ( K ` D ) -> ( ( `' K ` y ) e. ran G <-> ( `' K ` ( K ` D ) ) e. ran G ) )
37		id 22	. . . . . . . . . . . 12 |- ( y = ( K ` D ) -> y = ( K ` D ) )
38	35	fveq2d 6195	. . . . . . . . . . . 12 |- ( y = ( K ` D ) -> ( `' G ` ( `' K ` y ) ) = ( `' G ` ( `' K ` ( K ` D ) ) ) )
39	37, 38	eleq12d 2695	. . . . . . . . . . 11 |- ( y = ( K ` D ) -> ( y e. ( `' G ` ( `' K ` y ) ) <-> ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
40	39	notbid 308	. . . . . . . . . 10 |- ( y = ( K ` D ) -> ( -. y e. ( `' G ` ( `' K ` y ) ) <-> -. ( K ` D ) e. ( `' G ` ( `' K ` ( K ` D ) ) ) ) )
41	36, 40	anbi12d 747	. . . . . . . . 9 |- ( 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 ) ) ) ) ) )
42		fveq2 6191	. . . . . . . . . . . 12 |- ( w = y -> ( `' K ` w ) = ( `' K ` y ) )
43	42	eleq1d 2686	. . . . . . . . . . 11 |- ( w = y -> ( ( `' K ` w ) e. ran G <-> ( `' K ` y ) e. ran G ) )
44		id 22	. . . . . . . . . . . . 13 |- ( w = y -> w = y )
45	42	fveq2d 6195	. . . . . . . . . . . . 13 |- ( w = y -> ( `' G ` ( `' K ` w ) ) = ( `' G ` ( `' K ` y ) ) )
46	44, 45	eleq12d 2695	. . . . . . . . . . . 12 |- ( w = y -> ( w e. ( `' G ` ( `' K ` w ) ) <-> y e. ( `' G ` ( `' K ` y ) ) ) )
47	46	notbid 308	. . . . . . . . . . 11 |- ( w = y -> ( -. w e. ( `' G ` ( `' K ` w ) ) <-> -. y e. ( `' G ` ( `' K ` y ) ) ) )
48	43, 47	anbi12d 747	. . . . . . . . . 10 |- ( w = y -> ( ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) <-> ( ( `' K ` y ) e. ran G /\ -. y e. ( `' G ` ( `' K ` y ) ) ) ) )
49	48	cbvrabv 3199	. . . . . . . . 9 |- { 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 ) ) ) }
50	41, 49	elrab2 3366	. . . . . . . 8 |- ( ( 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 ) ) ) ) ) )
51		anass 681	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) ) ) )
52	50, 51	bitr4i 267	. . . . . . 7 |- ( ( 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	52	baib 944	. . . . . 6 |- ( ( ( 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 ) ) ) ) )
54	23, 34, 53	syl2anc 693	. . . . 5 |- ( ( ( 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 ) ) ) ) )
55	27, 1	syl6eq 2672	. . . . . . . . 9 |- ( ( ( 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 ) ) ) } ) )
56	55	fveq2d 6195	. . . . . . . 8 |- ( ( ( 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 ) ) ) } ) ) )
57		f1f1orn 6148	. . . . . . . . . . 11 |- ( G : ~P A -1-1-> U_ n e. om ( A ^m n ) -> G : ~P A -1-1-onto-> ran G )
58	3, 57	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ps ) -> G : ~P A -1-1-onto-> ran G )
59		f1ocnvfv1 6532	. . . . . . . . . 10 |- ( ( 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 ) ) ) } )
60	58, 14, 59	syl2anc 693	. . . . . . . . 9 |- ( ( 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 ) ) ) } )
61	60	adantr 481	. . . . . . . 8 |- ( ( ( 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 ) ) ) } )
62	56, 61	eqtrd 2656	. . . . . . 7 |- ( ( ( 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 ) ) ) } )
63	62	eleq2d 2687	. . . . . 6 |- ( ( ( 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 ) ) ) } ) )
64	63	notbid 308	. . . . 5 |- ( ( ( 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 ) ) ) } ) )
65	54, 64	bitrd 268	. . . 4 |- ( ( ( 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 ) ) ) } ) )
66	65	ex 450	. . 3 |- ( ( 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 ) ) ) } ) ) )
67	17, 66	mtoi 190	. 2 |- ( ( ph /\ ps ) -> -. D e. U_ n e. om ( x ^m n ) )
68	16, 67	eldifd 3585	1 |- ( ( ph /\ ps ) -> D e. ( U_ n e. om ( A ^m n ) \ U_ n e. om ( x ^m n ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {crab 2916   \ cdif 3571   C_ wss 3574   ~Pcpw 4158   U_ciun 4520   class class class wbr 4653   We wwe 5072   X. cxp 5112   `'ccnv 5113   ran crn 5115   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   omcom 7065   ^m cmap 7857   ~<_ cdom 7953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896

This theorem is referenced by:  pwfseqlem3  9482