Theorem domtriomlem 8874

Description: Lemma for domtriom 8875. (Contributed by Mario Carneiro, 9-Feb-2013.)

Hypotheses

Ref	Expression
domtriomlem.1	|- A e. _V
domtriomlem.2	|- B = { y | ( y C_ A /\ y ~~ ~P n ) }
domtriomlem.3	|- C = ( n e. om |-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )

Assertion

Ref	Expression
domtriomlem	|- ( -. A e. Fin -> om ~<_ A )

Distinct variable groups:   A, b, n, y   B, b   C, k, n   k, b   y, b

Allowed substitution hints:   A( k)   B( y, k, n)   C( y, b)

Proof of Theorem domtriomlem

Dummy variables c m j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		domtriomlem.2	. . . . 5 |- B = { y | ( y C_ A /\ y ~~ ~P n ) }
2		domtriomlem.1	. . . . . . 7 |- A e. _V
3	2	pwex 4605	. . . . . 6 |- ~P A e. _V
4		simpl 459	. . . . . . . 8 |- ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
5	4	ss2abi 3534	. . . . . . 7 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
6		df-pw 3982	. . . . . . 7 |- ~P A = { y | y C_ A }
7	5, 6	sseqtr4i 3498	. . . . . 6 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ ~P A
8	3, 7	ssexi 4567	. . . . 5 |- { y | ( y C_ A /\ y ~~ ~P n ) } e. _V
9	1, 8	eqeltri 2507	. . . 4 |- B e. _V
10		omex 8152	. . . . 5 |- om e. _V
11	10	enref 7607	. . . 4 |- om ~~ om
12	9, 11	axcc3 8870	. . 3 |- E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
13		nfv 1752	. . . . . . . 8 |- F/ n -. A e. Fin
14		nfra1 2807	. . . . . . . 8 |- F/ n A. n e. om ( B =/= (/) -> ( b ` n ) e. B )
15	13, 14	nfan 1985	. . . . . . 7 |- F/ n ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
16		nnfi 7769	. . . . . . . . . . . . . 14 |- ( n e. om -> n e. Fin )
17		pwfi 7873	. . . . . . . . . . . . . 14 |- ( n e. Fin <-> ~P n e. Fin )
18	16, 17	sylib 200	. . . . . . . . . . . . 13 |- ( n e. om -> ~P n e. Fin )
19		ficardom 8398	. . . . . . . . . . . . 13 |- ( ~P n e. Fin -> ( card ` ~P n ) e. om )
20		isinf 7789	. . . . . . . . . . . . . 14 |- ( -. A e. Fin -> A. m e. om E. y ( y C_ A /\ y ~~ m ) )
21		breq2 4425	. . . . . . . . . . . . . . . . 17 |- ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
22	21	anbi2d 709	. . . . . . . . . . . . . . . 16 |- ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
23	22	exbidv 1759	. . . . . . . . . . . . . . 15 |- ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24	23	rspcv 3179	. . . . . . . . . . . . . 14 |- ( ( card ` ~P n ) e. om -> ( A. m e. om E. y ( y C_ A /\ y ~~ m ) -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
25	20, 24	syl5 34	. . . . . . . . . . . . 13 |- ( ( card ` ~P n ) e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
26	18, 19, 25	3syl 18	. . . . . . . . . . . 12 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
27		finnum 8385	. . . . . . . . . . . . . . 15 |- ( ~P n e. Fin -> ~P n e. dom card )
28		cardid2 8390	. . . . . . . . . . . . . . 15 |- ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
29		entr 7626	. . . . . . . . . . . . . . . 16 |- ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
30	29	expcom 437	. . . . . . . . . . . . . . 15 |- ( ( card ` ~P n ) ~~ ~P n -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
31	18, 27, 28, 30	4syl 19	. . . . . . . . . . . . . 14 |- ( n e. om -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
32	31	anim2d 568	. . . . . . . . . . . . 13 |- ( n e. om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
33	32	eximdv 1755	. . . . . . . . . . . 12 |- ( n e. om -> ( E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
34	26, 33	syld 46	. . . . . . . . . . 11 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
35	1	neeq1i 2710	. . . . . . . . . . . 12 |- ( B =/= (/) <-> { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) )
36		abn0 3782	. . . . . . . . . . . 12 |- ( { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
37	35, 36	bitri 253	. . . . . . . . . . 11 |- ( B =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
38	34, 37	syl6ibr 231	. . . . . . . . . 10 |- ( n e. om -> ( -. A e. Fin -> B =/= (/) ) )
39	38	com12 33	. . . . . . . . 9 |- ( -. A e. Fin -> ( n e. om -> B =/= (/) ) )
40	39	adantr 467	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> B =/= (/) ) )
41		rsp 2792	. . . . . . . . 9 |- ( A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
42	41	adantl 468	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
43	40, 42	mpdd 42	. . . . . . 7 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> ( b ` n ) e. B ) )
44	15, 43	ralrimi 2826	. . . . . 6 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
45	44	3adant2 1025	. . . . 5 |- ( ( -. A e. Fin /\ b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
46	45	3expib 1209	. . . 4 |- ( -. A e. Fin -> ( ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B ) )
47	46	eximdv 1755	. . 3 |- ( -. A e. Fin -> ( E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> E. b A. n e. om ( b ` n ) e. B ) )
48	12, 47	mpi 21	. 2 |- ( -. A e. Fin -> E. b A. n e. om ( b ` n ) e. B )
49		axcc2 8869	. . . . 5 |- E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
50		simp2 1007	. . . . . . . 8 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> c Fn om )
51		nfra1 2807	. . . . . . . . . . 11 |- F/ n A. n e. om ( b ` n ) e. B
52		nfra1 2807	. . . . . . . . . . 11 |- F/ n A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
53	51, 52	nfan 1985	. . . . . . . . . 10 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
54		fvex 5889	. . . . . . . . . . . . . . . 16 |- ( b ` n ) e. _V
55		sseq1 3486	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
56		breq1 4424	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
57	55, 56	anbi12d 716	. . . . . . . . . . . . . . . 16 |- ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
58	54, 57, 1	elab2 3222	. . . . . . . . . . . . . . 15 |- ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
59	58	simprbi 466	. . . . . . . . . . . . . 14 |- ( ( b ` n ) e. B -> ( b ` n ) ~~ ~P n )
60	59	ralimi 2819	. . . . . . . . . . . . 13 |- ( A. n e. om ( b ` n ) e. B -> A. n e. om ( b ` n ) ~~ ~P n )
61		fveq2 5879	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( b ` n ) = ( b ` k ) )
62		pweq 3983	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ~P n = ~P k )
63	61, 62	breq12d 4434	. . . . . . . . . . . . . . . 16 |- ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
64	63	cbvralv 3056	. . . . . . . . . . . . . . 15 |- ( A. n e. om ( b ` n ) ~~ ~P n <-> A. k e. om ( b ` k ) ~~ ~P k )
65		peano2 6725	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> suc n e. om )
66		omelon 8155	. . . . . . . . . . . . . . . . . . 19 |- om e. On
67	66	onelssi 5548	. . . . . . . . . . . . . . . . . 18 |- ( suc n e. om -> suc n C_ om )
68		ssralv 3526	. . . . . . . . . . . . . . . . . 18 |- ( suc n C_ om -> ( A. k e. om ( b ` k ) ~~ ~P k -> A. k e. suc n ( b ` k ) ~~ ~P k ) )
69	65, 67, 68	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> A. k e. suc n ( b ` k ) ~~ ~P k ) )
70		pwsdompw 8636	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
71	70	ex 436	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. k e. suc n ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
72	69, 71	syld 46	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
73		sdomdif 7724	. . . . . . . . . . . . . . . 16 |- ( U_ k e. n ( b ` k ) ~< ( b ` n ) -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) )
74	72, 73	syl6 35	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
75	64, 74	syl5bi 221	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76		difss 3593	. . . . . . . . . . . . . . . . 17 |- ( ( b ` n ) \ U_ k e. n ( b ` k ) ) C_ ( b ` n )
77	54, 76	ssexi 4567	. . . . . . . . . . . . . . . 16 |- ( ( b ` n ) \ U_ k e. n ( b ` k ) ) e. _V
78		domtriomlem.3	. . . . . . . . . . . . . . . . 17 |- C = ( n e. om |-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
79	78	fvmpt2 5971	. . . . . . . . . . . . . . . 16 |- ( ( n e. om /\ ( ( b ` n ) \ U_ k e. n ( b ` k ) ) e. _V ) -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
80	77, 79	mpan2 676	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
81	80	neeq1d 2702	. . . . . . . . . . . . . 14 |- ( n e. om -> ( ( C ` n ) =/= (/) <-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
82	75, 81	sylibrd 238	. . . . . . . . . . . . 13 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( C ` n ) =/= (/) ) )
83	60, 82	syl5com 32	. . . . . . . . . . . 12 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( C ` n ) =/= (/) ) )
84	83	adantr 467	. . . . . . . . . . 11 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( n e. om -> ( C ` n ) =/= (/) ) )
85		rsp 2792	. . . . . . . . . . . 12 |- ( A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) -> ( n e. om -> ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) )
86	85	adantl 468	. . . . . . . . . . 11 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( n e. om -> ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) )
87	84, 86	mpdd 42	. . . . . . . . . 10 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( n e. om -> ( c ` n ) e. ( C ` n ) ) )
88	53, 87	ralrimi 2826	. . . . . . . . 9 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> A. n e. om ( c ` n ) e. ( C ` n ) )
89	88	3adant2 1025	. . . . . . . 8 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> A. n e. om ( c ` n ) e. ( C ` n ) )
90	50, 89	jca 535	. . . . . . 7 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) )
91	90	3expib 1209	. . . . . 6 |- ( A. n e. om ( b ` n ) e. B -> ( ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) ) )
92	91	eximdv 1755	. . . . 5 |- ( A. n e. om ( b ` n ) e. B -> ( E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> E. c ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) ) )
93	49, 92	mpi 21	. . . 4 |- ( A. n e. om ( b ` n ) e. B -> E. c ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) )
94		simp2 1007	. . . . . . . . . 10 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> c Fn om )
95		nfra1 2807	. . . . . . . . . . . . 13 |- F/ n A. n e. om ( c ` n ) e. ( C ` n )
96	51, 95	nfan 1985	. . . . . . . . . . . 12 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) )
97		rsp 2792	. . . . . . . . . . . . . . . 16 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( C ` n ) ) )
98	97	com12 33	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( C ` n ) ) )
99		rsp 2792	. . . . . . . . . . . . . . . . . 18 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( b ` n ) e. B ) )
100	99	com12 33	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( b ` n ) e. B ) )
101	80	eleq2d 2493	. . . . . . . . . . . . . . . . . . 19 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
102		eldifi 3588	. . . . . . . . . . . . . . . . . . 19 |- ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. ( b ` n ) )
103	101, 102	syl6bi 232	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` n ) ) )
104	58	simplbi 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( b ` n ) e. B -> ( b ` n ) C_ A )
105	104	sseld 3464	. . . . . . . . . . . . . . . . . 18 |- ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
106	103, 105	syl9 74	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
107	100, 106	syld 46	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
108	107	com23 82	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) -> ( A. n e. om ( b ` n ) e. B -> ( c ` n ) e. A ) ) )
109	98, 108	syld 46	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( A. n e. om ( b ` n ) e. B -> ( c ` n ) e. A ) ) )
110	109	com13 84	. . . . . . . . . . . . 13 |- ( A. n e. om ( b ` n ) e. B -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. A ) ) )
111	110	imp 431	. . . . . . . . . . . 12 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( n e. om -> ( c ` n ) e. A ) )
112	96, 111	ralrimi 2826	. . . . . . . . . . 11 |- ( ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> A. n e. om ( c ` n ) e. A )
113	112	3adant2 1025	. . . . . . . . . 10 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> A. n e. om ( c ` n ) e. A )
114		ffnfv 6062	. . . . . . . . . 10 |- ( c : om --> A <-> ( c Fn om /\ A. n e. om ( c ` n ) e. A ) )
115	94, 113, 114	sylanbrc 669	. . . . . . . . 9 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> c : om --> A )
116		nfv 1752	. . . . . . . . . . . 12 |- F/ n k e. om
117		nnord 6712	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
118		nnord 6712	. . . . . . . . . . . . . . . 16 |- ( n e. om -> Ord n )
119		ordtri3or 5472	. . . . . . . . . . . . . . . 16 |- ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
120	117, 118, 119	syl2an 480	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ n e. om ) -> ( k e. n \/ k = n \/ n e. k ) )
121	97, 101	mpbidi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
122	95, 121	ralrimi 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> A. n e. om ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
123		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( c ` n ) = ( c ` k ) )
124		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k = j -> ( b ` k ) = ( b ` j ) )
125	124	cbviunv 4336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
126		iuneq1 4311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
127	125, 126	syl5eq 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
128	61, 127	difeq12d 3585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
129	123, 128	eleq12d 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( n = k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) <-> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
130	129	rspccv 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. n e. om ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( k e. om -> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
131	122, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
132	131	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
133	132	3ad2ant1 1027	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
134		eldifi 3588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
135		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( b ` k ) <-> ( c ` n ) e. ( b ` k ) ) )
136	134, 135	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
137	136	3ad2ant3 1029	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
138	133, 137	syld 46	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` k ) ) )
139	138	imp 431	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. ( b ` k ) )
140		ssiun2 4340	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
141	140	sseld 3464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. n -> ( ( c ` n ) e. ( b ` k ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
142	139, 141	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. n -> ( ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
143	142	3impib 1204	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. n /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. U_ k e. n ( b ` k ) )
144	121	com12 33	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
145	144	3ad2ant2 1028	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
146	145	imp 431	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
147	146	eldifbd 3450	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> -. ( c ` n ) e. U_ k e. n ( b ` k ) )
148	147	3adant1 1024	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. n /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> -. ( c ` n ) e. U_ k e. n ( b ` k ) )
149	143, 148	pm2.21dd 178	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. n /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> k = n )
150	149	3exp 1205	. . . . . . . . . . . . . . . . . 18 |- ( k e. n -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
151		2a1 29	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
152		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = n -> ( b ` j ) = ( b ` n ) )
153	152	ssiun2s 4341	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
154	153	sseld 3464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
155	102, 154	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
156	146, 155	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. k -> ( ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
157	156	3impib 1204	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. k /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> ( c ` n ) e. U_ j e. k ( b ` j ) )
158		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) <-> ( c ` n ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
159		eldifn 3589	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` n ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) )
160	158, 159	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) ) )
161	160	3ad2ant3 1029	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) ) )
162	133, 161	syld 46	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) ) )
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. k -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) ) ) )
164	163	3imp 1200	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. k /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) )
165	157, 164	pm2.21dd 178	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. k /\ ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> k = n )
166	165	3exp 1205	. . . . . . . . . . . . . . . . . 18 |- ( n e. k -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
167	150, 151, 166	3jaoi 1328	. . . . . . . . . . . . . . . . 17 |- ( ( k e. n \/ k = n \/ n e. k ) -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
168	167	com12 33	. . . . . . . . . . . . . . . 16 |- ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( ( k e. n \/ k = n \/ n e. k ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
169	168	3expia 1208	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> ( ( k e. n \/ k = n \/ n e. k ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) ) )
170	120, 169	mpid 43	. . . . . . . . . . . . . 14 |- ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
171	170	com3r 83	. . . . . . . . . . . . 13 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
172	171	expd 438	. . . . . . . . . . . 12 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> ( n e. om -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) ) )
173	95, 116, 172	ralrimd 2830	. . . . . . . . . . 11 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
174	173	ralrimiv 2838	. . . . . . . . . 10 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) )
175	174	3ad2ant3 1029	. . . . . . . . 9 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) )
176		dff13 6172	. . . . . . . . 9 |- ( c : om -1-1-> A <-> ( c : om --> A /\ A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
177	115, 175, 176	sylanbrc 669	. . . . . . . 8 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> c : om -1-1-> A )
178		19.8a 1909	. . . . . . . 8 |- ( c : om -1-1-> A -> E. c c : om -1-1-> A )
179	177, 178	syl 17	. . . . . . 7 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> E. c c : om -1-1-> A )
180	2	brdom 7587	. . . . . . 7 |- ( om ~<_ A <-> E. c c : om -1-1-> A )
181	179, 180	sylibr 216	. . . . . 6 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A )
182	181	3expib 1209	. . . . 5 |- ( A. n e. om ( b ` n ) e. B -> ( ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A ) )
183	182	exlimdv 1769	. . . 4 |- ( A. n e. om ( b ` n ) e. B -> ( E. c ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A ) )
184	93, 183	mpd 15	. . 3 |- ( A. n e. om ( b ` n ) e. B -> om ~<_ A )
185	184	exlimiv 1767	. 2 |- ( E. b A. n e. om ( b ` n ) e. B -> om ~<_ A )
186	48, 185	syl 17	1 |- ( -. A e. Fin -> om ~<_ A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   \/ w3o 982   /\ w3a 983   = wceq 1438   E.wex 1660   e. wcel 1869   {cab 2408   =/= wne 2619   A.wral 2776   _Vcvv 3082   \ cdif 3434   C_ wss 3437   (/)c0 3762   ~Pcpw 3980   U_ciun 4297   class class class wbr 4421   |-> cmpt 4480   dom cdm 4851   Ord word 5439   suc csuc 5442   Fn wfn 5594   -->wf 5595   -1-1->wf1 5596   ` cfv 5599   omcom 6704   ~~ cen 7572   ~<_ cdom 7573   ~< csdm 7574   Fincfn 7575   cardccrd 8372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-cc 8867

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-card 8376  df-cda 8600

This theorem is referenced by:  domtriom  8875