pwfseqlem4

Description: Lemma for pwfseq . Derive a final contradiction from the function F in pwfseqlem3 . Applying fpwwe2 to it, we get a certain maximal well-ordered subset Z , but the defining property ( Z F ( WZ ) ) e. Z contradicts our assumption on F , so we are reduced to the case of Z finite. This too is a contradiction, though, because Z and its preimage under ( WZ ) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by Matthew House, 10-Sep-2025)

	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 } ) ) )
	pwfseqlem4.w	\|- W = { <. a , s >. \| ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = b ) ) }
	pwfseqlem4.z	\|- Z = U. dom W
Assertion	pwfseqlem4	\|- -. ph

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		pwfseqlem4.w	\|- W = { <. a , s >. \| ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = b ) ) }
9		pwfseqlem4.z	\|- Z = U. dom W
10		eqid	\|- Z = Z
11		eqid	\|- ( W ` Z ) = ( W ` Z )
12	10 11	pm3.2i	\|- ( Z = Z /\ ( W ` Z ) = ( W ` Z ) )
13		omex	\|- _om e. _V
14		ovex	\|- ( A ^m n ) e. _V
15	13 14	iunex	\|- U_ n e. _om ( A ^m n ) e. _V
16		f1dmex	\|- ( ( G : ~P A -1-1-> U_ n e. _om ( A ^m n ) /\ U_ n e. _om ( A ^m n ) e. _V ) -> ~P A e. _V )
17	1 15 16	sylancl	\|- ( ph -> ~P A e. _V )
18		pwexb	\|- ( A e. _V <-> ~P A e. _V )
19	17 18	sylibr	\|- ( ph -> A e. _V )
20	1 2 3 4 5 6 7	pwfseqlem4a	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A )
21	8 19 20 9	fpwwe2	\|- ( ph -> ( ( Z W ( W ` Z ) /\ ( Z F ( W ` Z ) ) e. Z ) <-> ( Z = Z /\ ( W ` Z ) = ( W ` Z ) ) ) )
22	12 21	mpbiri	\|- ( ph -> ( Z W ( W ` Z ) /\ ( Z F ( W ` Z ) ) e. Z ) )
23	22	simpld	\|- ( ph -> Z W ( W ` Z ) )
24	8 19	fpwwe2lem2	\|- ( ph -> ( Z W ( W ` Z ) <-> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) ) )
25	23 24	mpbid	\|- ( ph -> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) )
26		id	\|- ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
27	26	3expa	\|- ( ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( W ` Z ) We Z ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
28	27	adantrr	\|- ( ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
29	25 28	syl	\|- ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
30	22	simprd	\|- ( ph -> ( Z F ( W ` Z ) ) e. Z )
31	25	simpld	\|- ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) )
32	31	simpld	\|- ( ph -> Z C_ A )
33	19 32	ssexd	\|- ( ph -> Z e. _V )
34		fvexd	\|- ( ph -> ( W ` Z ) e. _V )
35		simpl	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> a = Z )
36	35	sseq1d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( a C_ A <-> Z C_ A ) )
37		simpr	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> s = ( W ` Z ) )
38	35	sqxpeqd	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( a X. a ) = ( Z X. Z ) )
39	37 38	sseq12d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( s C_ ( a X. a ) <-> ( W ` Z ) C_ ( Z X. Z ) ) )
40	37 35	weeq12d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( s We a <-> ( W ` Z ) We Z ) )
41	36 39 40	3anbi123d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) <-> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) ) )
42		oveq12	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( a F s ) = ( Z F ( W ` Z ) ) )
43	42 35	eleq12d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( a F s ) e. a <-> ( Z F ( W ` Z ) ) e. Z ) )
44	35	breq1d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( a ~< _om <-> Z ~< _om ) )
45	43 44	imbi12d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( ( a F s ) e. a -> a ~< _om ) <-> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
46	41 45	imbi12d	\|- ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) -> ( ( a F s ) e. a -> a ~< _om ) ) <-> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) ) )
47		omelon	\|- _om e. On
48		onenon	\|- ( _om e. On -> _om e. dom card )
49	47 48	ax-mp	\|- _om e. dom card
50		simpr3	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> s We a )
51	50	19.8ad	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> E. s s We a )
52		ween	\|- ( a e. dom card <-> E. s s We a )
53	51 52	sylibr	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> a e. dom card )
54		domtri2	\|- ( ( _om e. dom card /\ a e. dom card ) -> ( _om ~<_ a <-> -. a ~< _om ) )
55	49 53 54	sylancr	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a <-> -. a ~< _om ) )
56		nfv	\|- F/ r ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) )
57		nfcv	\|- F/_ r a
58		nfmpo2	\|- F/_ r ( x e. _V , r e. _V \|-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` \|^\| { z e. _om \| -. ( D ` z ) e. x } ) ) )
59	7 58	nfcxfr	\|- F/_ r F
60		nfcv	\|- F/_ r s
61	57 59 60	nfov	\|- F/_ r ( a F s )
62	61	nfel1	\|- F/ r ( a F s ) e. ( A \ a )
63	56 62	nfim	\|- F/ r ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
64		sseq1	\|- ( r = s -> ( r C_ ( a X. a ) <-> s C_ ( a X. a ) ) )
65		weeq1	\|- ( r = s -> ( r We a <-> s We a ) )
66	64 65	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 ) ) )
67	66	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 ) ) )
68	67	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 ) ) ) )
69		oveq2	\|- ( r = s -> ( a F r ) = ( a F s ) )
70	69	eleq1d	\|- ( r = s -> ( ( a F r ) e. ( A \ a ) <-> ( a F s ) e. ( A \ a ) ) )
71	68 70	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 ) ) ) )
72		nfv	\|- F/ x ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) )
73		nfcv	\|- F/_ x a
74		nfmpo1	\|- F/_ x ( x e. _V , r e. _V \|-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` \|^\| { z e. _om \| -. ( D ` z ) e. x } ) ) )
75	7 74	nfcxfr	\|- F/_ x F
76		nfcv	\|- F/_ x r
77	73 75 76	nfov	\|- F/_ x ( a F r )
78	77	nfel1	\|- F/ x ( a F r ) e. ( A \ a )
79	72 78	nfim	\|- F/ x ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
80		sseq1	\|- ( x = a -> ( x C_ A <-> a C_ A ) )
81		xpeq12	\|- ( ( x = a /\ x = a ) -> ( x X. x ) = ( a X. a ) )
82	81	anidms	\|- ( x = a -> ( x X. x ) = ( a X. a ) )
83	82	sseq2d	\|- ( x = a -> ( r C_ ( x X. x ) <-> r C_ ( a X. a ) ) )
84		weeq2	\|- ( x = a -> ( r We x <-> r We a ) )
85	80 83 84	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 ) ) )
86		breq2	\|- ( x = a -> ( _om ~<_ x <-> _om ~<_ a ) )
87	85 86	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 ) ) )
88	4 87	bitrid	\|- ( x = a -> ( ps <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
89	88	anbi2d	\|- ( x = a -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) )
90		oveq1	\|- ( x = a -> ( x F r ) = ( a F r ) )
91		difeq2	\|- ( x = a -> ( A \ x ) = ( A \ a ) )
92	90 91	eleq12d	\|- ( x = a -> ( ( x F r ) e. ( A \ x ) <-> ( a F r ) e. ( A \ a ) ) )
93	89 92	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 ) ) ) )
94	1 2 3 4 5 6 7	pwfseqlem3	\|- ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )
95	79 93 94	chvarfv	\|- ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
96	63 71 95	chvarfv	\|- ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
97	96	eldifbd	\|- ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> -. ( a F s ) e. a )
98	97	expr	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a -> -. ( a F s ) e. a ) )
99	55 98	sylbird	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( -. a ~< _om -> -. ( a F s ) e. a ) )
100	99	con4d	\|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( ( a F s ) e. a -> a ~< _om ) )
101	100	ex	\|- ( ph -> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) -> ( ( a F s ) e. a -> a ~< _om ) ) )
102	33 34 46 101	vtocl2d	\|- ( ph -> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
103	29 30 102	mp2d	\|- ( ph -> Z ~< _om )
104		isfinite	\|- ( Z e. Fin <-> Z ~< _om )
105	103 104	sylibr	\|- ( ph -> Z e. Fin )
106		fvex	\|- ( W ` Z ) e. _V
107	1 2 3 4 5 6 7	pwfseqlem2	\|- ( ( Z e. Fin /\ ( W ` Z ) e. _V ) -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
108	105 106 107	sylancl	\|- ( ph -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
109	108 30	eqeltrrd	\|- ( ph -> ( H ` ( card ` Z ) ) e. Z )
110	8 19 23	fpwwe2lem3	\|- ( ( ph /\ ( H ` ( card ` Z ) ) e. Z ) -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` Z ) ) )
111	109 110	mpdan	\|- ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` Z ) ) )
112		cnvimass	\|- ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ dom ( W ` Z )
113	31	simprd	\|- ( ph -> ( W ` Z ) C_ ( Z X. Z ) )
114		dmss	\|- ( ( W ` Z ) C_ ( Z X. Z ) -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
115	113 114	syl	\|- ( ph -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
116		dmxpss	\|- dom ( Z X. Z ) C_ Z
117	115 116	sstrdi	\|- ( ph -> dom ( W ` Z ) C_ Z )
118	112 117	sstrid	\|- ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z )
119	105 118	ssfid	\|- ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin )
120	106	inex1	\|- ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) e. _V
121	1 2 3 4 5 6 7	pwfseqlem2	\|- ( ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin /\ ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) e. _V ) -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
122	119 120 121	sylancl	\|- ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
123	111 122	eqtr3d	\|- ( ph -> ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
124		f1of1	\|- ( H : _om -1-1-onto-> X -> H : _om -1-1-> X )
125	3 124	syl	\|- ( ph -> H : _om -1-1-> X )
126		ficardom	\|- ( Z e. Fin -> ( card ` Z ) e. _om )
127	105 126	syl	\|- ( ph -> ( card ` Z ) e. _om )
128		ficardom	\|- ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
129	119 128	syl	\|- ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
130		f1fveq	\|- ( ( H : _om -1-1-> X /\ ( ( card ` Z ) e. _om /\ ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om ) ) -> ( ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) <-> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
131	125 127 129 130	syl12anc	\|- ( ph -> ( ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) <-> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
132	123 131	mpbid	\|- ( ph -> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) )
133	132	eqcomd	\|- ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) )
134		finnum	\|- ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
135	119 134	syl	\|- ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
136		finnum	\|- ( Z e. Fin -> Z e. dom card )
137	105 136	syl	\|- ( ph -> Z e. dom card )
138		carden2	\|- ( ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card /\ Z e. dom card ) -> ( ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) <-> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
139	135 137 138	syl2anc	\|- ( ph -> ( ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) <-> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
140	133 139	mpbid	\|- ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
141		dfpss2	\|- ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z /\ -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
142	141	baib	\|- ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
143	118 142	syl	\|- ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
144		php3	\|- ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z )
145		sdomnen	\|- ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
146	144 145	syl	\|- ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
147	146	ex	\|- ( Z e. Fin -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
148	105 147	syl	\|- ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
149	143 148	sylbird	\|- ( ph -> ( -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
150	140 149	mt4d	\|- ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z )
151	109 150	eleqtrrd	\|- ( ph -> ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) )
152		fvex	\|- ( H ` ( card ` Z ) ) e. _V
153	152	eliniseg	\|- ( ( H ` ( card ` Z ) ) e. _V -> ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) ) )
154	152 153	ax-mp	\|- ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
155	151 154	sylib	\|- ( ph -> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
156	25	simprd	\|- ( ph -> ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) )
157	156	simpld	\|- ( ph -> ( W ` Z ) We Z )
158		weso	\|- ( ( W ` Z ) We Z -> ( W ` Z ) Or Z )
159	157 158	syl	\|- ( ph -> ( W ` Z ) Or Z )
160		sonr	\|- ( ( ( W ` Z ) Or Z /\ ( H ` ( card ` Z ) ) e. Z ) -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
161	159 109 160	syl2anc	\|- ( ph -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
162	155 161	pm2.65i	\|- -. ph

Metamath Proof Explorer

Theorem pwfseqlem4

Proof