Theorem domtriomlem 8774

Description: Lemma for domtriom 8775. (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 4576	. . . . . 6 |- ~P A e. _V
4		simpl 455	. . . . . . . 8 |- ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
5	4	ss2abi 3510	. . . . . . 7 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
6		df-pw 3956	. . . . . . 7 |- ~P A = { y | y C_ A }
7	5, 6	sseqtr4i 3474	. . . . . 6 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ ~P A
8	3, 7	ssexi 4538	. . . . 5 |- { y | ( y C_ A /\ y ~~ ~P n ) } e. _V
9	1, 8	eqeltri 2486	. . . 4 |- B e. _V
10		omex 8013	. . . . 5 |- om e. _V
11	10	enref 7506	. . . 4 |- om ~~ om
12	9, 11	axcc3 8770	. . 3 |- E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
13		nfv 1728	. . . . . . . 8 |- F/ n -. A e. Fin
14		nfra1 2784	. . . . . . . 8 |- F/ n A. n e. om ( B =/= (/) -> ( b ` n ) e. B )
15	13, 14	nfan 1956	. . . . . . 7 |- F/ n ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
16		nnfi 7668	. . . . . . . . . . . . . 14 |- ( n e. om -> n e. Fin )
17		pwfi 7769	. . . . . . . . . . . . . 14 |- ( n e. Fin <-> ~P n e. Fin )
18	16, 17	sylib 196	. . . . . . . . . . . . 13 |- ( n e. om -> ~P n e. Fin )
19		ficardom 8294	. . . . . . . . . . . . 13 |- ( ~P n e. Fin -> ( card ` ~P n ) e. om )
20		isinf 7688	. . . . . . . . . . . . . 14 |- ( -. A e. Fin -> A. m e. om E. y ( y C_ A /\ y ~~ m ) )
21		breq2 4398	. . . . . . . . . . . . . . . . 17 |- ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
22	21	anbi2d 702	. . . . . . . . . . . . . . . 16 |- ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
23	22	exbidv 1735	. . . . . . . . . . . . . . 15 |- ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24	23	rspcv 3155	. . . . . . . . . . . . . 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 30	. . . . . . . . . . . . 13 |- ( ( card ` ~P n ) e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
26	18, 19, 25	3syl 20	. . . . . . . . . . . 12 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
27		finnum 8281	. . . . . . . . . . . . . . 15 |- ( ~P n e. Fin -> ~P n e. dom card )
28		cardid2 8286	. . . . . . . . . . . . . . 15 |- ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
29		entr 7525	. . . . . . . . . . . . . . . 16 |- ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
30	29	expcom 433	. . . . . . . . . . . . . . 15 |- ( ( card ` ~P n ) ~~ ~P n -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
31	18, 27, 28, 30	4syl 21	. . . . . . . . . . . . . 14 |- ( n e. om -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
32	31	anim2d 563	. . . . . . . . . . . . 13 |- ( n e. om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
33	32	eximdv 1731	. . . . . . . . . . . 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 42	. . . . . . . . . . 11 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
35	1	neeq1i 2688	. . . . . . . . . . . 12 |- ( B =/= (/) <-> { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) )
36		abn0 3757	. . . . . . . . . . . 12 |- ( { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
37	35, 36	bitri 249	. . . . . . . . . . 11 |- ( B =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
38	34, 37	syl6ibr 227	. . . . . . . . . 10 |- ( n e. om -> ( -. A e. Fin -> B =/= (/) ) )
39	38	com12 29	. . . . . . . . 9 |- ( -. A e. Fin -> ( n e. om -> B =/= (/) ) )
40	39	adantr 463	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> B =/= (/) ) )
41		rsp 2769	. . . . . . . . 9 |- ( A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
42	41	adantl 464	. . . . . . . 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 38	. . . . . . 7 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> ( b ` n ) e. B ) )
44	15, 43	ralrimi 2803	. . . . . 6 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
45	44	3adant2 1016	. . . . 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 1200	. . . 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 1731	. . 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 18	. 2 |- ( -. A e. Fin -> E. b A. n e. om ( b ` n ) e. B )
49		axcc2 8769	. . . . 5 |- E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
50		simp2 998	. . . . . . . 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 2784	. . . . . . . . . . 11 |- F/ n A. n e. om ( b ` n ) e. B
52		nfra1 2784	. . . . . . . . . . 11 |- F/ n A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
53	51, 52	nfan 1956	. . . . . . . . . 10 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
54		fvex 5815	. . . . . . . . . . . . . . . 16 |- ( b ` n ) e. _V
55		sseq1 3462	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
56		breq1 4397	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
57	55, 56	anbi12d 709	. . . . . . . . . . . . . . . 16 |- ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
58	54, 57, 1	elab2 3198	. . . . . . . . . . . . . . 15 |- ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
59	58	simprbi 462	. . . . . . . . . . . . . 14 |- ( ( b ` n ) e. B -> ( b ` n ) ~~ ~P n )
60	59	ralimi 2796	. . . . . . . . . . . . 13 |- ( A. n e. om ( b ` n ) e. B -> A. n e. om ( b ` n ) ~~ ~P n )
61		fveq2 5805	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( b ` n ) = ( b ` k ) )
62		pweq 3957	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ~P n = ~P k )
63	61, 62	breq12d 4407	. . . . . . . . . . . . . . . 16 |- ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
64	63	cbvralv 3033	. . . . . . . . . . . . . . 15 |- ( A. n e. om ( b ` n ) ~~ ~P n <-> A. k e. om ( b ` k ) ~~ ~P k )
65		peano2 6658	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> suc n e. om )
66		omelon 8016	. . . . . . . . . . . . . . . . . . 19 |- om e. On
67	66	onelssi 4929	. . . . . . . . . . . . . . . . . 18 |- ( suc n e. om -> suc n C_ om )
68		ssralv 3502	. . . . . . . . . . . . . . . . . 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 20	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> A. k e. suc n ( b ` k ) ~~ ~P k ) )
70		pwsdompw 8536	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
71	70	ex 432	. . . . . . . . . . . . . . . . 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 42	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
73		sdomdif 7623	. . . . . . . . . . . . . . . 16 |- ( U_ k e. n ( b ` k ) ~< ( b ` n ) -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) )
74	72, 73	syl6 31	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
75	64, 74	syl5bi 217	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76		difss 3569	. . . . . . . . . . . . . . . . 17 |- ( ( b ` n ) \ U_ k e. n ( b ` k ) ) C_ ( b ` n )
77	54, 76	ssexi 4538	. . . . . . . . . . . . . . . 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 5897	. . . . . . . . . . . . . . . 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 669	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
81	80	neeq1d 2680	. . . . . . . . . . . . . 14 |- ( n e. om -> ( ( C ` n ) =/= (/) <-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
82	75, 81	sylibrd 234	. . . . . . . . . . . . 13 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( C ` n ) =/= (/) ) )
83	60, 82	syl5com 28	. . . . . . . . . . . 12 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( C ` n ) =/= (/) ) )
84	83	adantr 463	. . . . . . . . . . 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 2769	. . . . . . . . . . . 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 464	. . . . . . . . . . 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 38	. . . . . . . . . 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 2803	. . . . . . . . 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 1016	. . . . . . . 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 530	. . . . . . 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 1200	. . . . . 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 1731	. . . . 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 18	. . . 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 998	. . . . . . . . . 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 2784	. . . . . . . . . . . . 13 |- F/ n A. n e. om ( c ` n ) e. ( C ` n )
96	51, 95	nfan 1956	. . . . . . . . . . . 12 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) )
97		rsp 2769	. . . . . . . . . . . . . . . 16 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( C ` n ) ) )
98	97	com12 29	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( C ` n ) ) )
99		rsp 2769	. . . . . . . . . . . . . . . . . 18 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( b ` n ) e. B ) )
100	99	com12 29	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( b ` n ) e. B ) )
101	80	eleq2d 2472	. . . . . . . . . . . . . . . . . . 19 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
102		eldifi 3564	. . . . . . . . . . . . . . . . . . 19 |- ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. ( b ` n ) )
103	101, 102	syl6bi 228	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` n ) ) )
104	58	simplbi 458	. . . . . . . . . . . . . . . . . . 19 |- ( ( b ` n ) e. B -> ( b ` n ) C_ A )
105	104	sseld 3440	. . . . . . . . . . . . . . . . . 18 |- ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
106	103, 105	syl9 70	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
107	100, 106	syld 42	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
108	107	com23 78	. . . . . . . . . . . . . . 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 42	. . . . . . . . . . . . . 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 80	. . . . . . . . . . . . 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 427	. . . . . . . . . . . 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 2803	. . . . . . . . . . 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 1016	. . . . . . . . . 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 5992	. . . . . . . . . 10 |- ( c : om --> A <-> ( c Fn om /\ A. n e. om ( c ` n ) e. A ) )
115	94, 113, 114	sylanbrc 662	. . . . . . . . 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 1728	. . . . . . . . . . . 12 |- F/ n k e. om
117		nnord 6646	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
118		nnord 6646	. . . . . . . . . . . . . . . 16 |- ( n e. om -> Ord n )
119		ordtri3or 4853	. . . . . . . . . . . . . . . 16 |- ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
120	117, 118, 119	syl2an 475	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ n e. om ) -> ( k e. n \/ k = n \/ n e. k ) )
121	97, 101	mpbidi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( c ` n ) = ( c ` k ) )
124		fveq2 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k = j -> ( b ` k ) = ( b ` j ) )
125	124	cbviunv 4309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
126		iuneq1 4284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
127	125, 126	syl5eq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
128	61, 127	difeq12d 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
129	123, 128	eleq12d 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3156	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 29	. . . . . . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . . . . . . . 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 3564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
135		eleq1 2474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( b ` k ) <-> ( c ` n ) e. ( b ` k ) ) )
136	134, 135	syl5ib 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
137	136	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . . . 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 42	. . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . 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 4313	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
141	140	sseld 3440	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. n -> ( ( c ` n ) e. ( b ` k ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
142	139, 141	syl5 30	. . . . . . . . . . . . . . . . . . . . 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 1195	. . . . . . . . . . . . . . . . . . . 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 29	. . . . . . . . . . . . . . . . . . . . . . . 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 1019	. . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . 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 3426	. . . . . . . . . . . . . . . . . . . . 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 1015	. . . . . . . . . . . . . . . . . . . 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 174	. . . . . . . . . . . . . . . . . . 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 1196	. . . . . . . . . . . . . . . . . 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		ax-1 6	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) )
152	151	a1d 25	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
153		fveq2 5805	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = n -> ( b ` j ) = ( b ` n ) )
154	153	ssiun2s 4314	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
155	154	sseld 3440	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
156	102, 155	syl5 30	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
157	146, 156	syl5 30	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
158	157	3impib 1195	. . . . . . . . . . . . . . . . . . . 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 ) )
159		eleq1 2474	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
160		eldifn 3565	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` n ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) )
161	159, 160	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
162	161	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
163	133, 162	syld 42	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
164	163	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 ) ) ) )
165	164	3imp 1191	. . . . . . . . . . . . . . . . . . . 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 ) )
166	158, 165	pm2.21dd 174	. . . . . . . . . . . . . . . . . . 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 )
167	166	3exp 1196	. . . . . . . . . . . . . . . . . 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 ) ) )
168	150, 152, 167	3jaoi 1293	. . . . . . . . . . . . . . . . 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 ) ) )
169	168	com12 29	. . . . . . . . . . . . . . . 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 ) ) )
170	169	3expia 1199	. . . . . . . . . . . . . . 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 ) ) ) )
171	120, 170	mpid 39	. . . . . . . . . . . . . 14 |- ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
172	171	com3r 79	. . . . . . . . . . . . 13 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
173	172	expd 434	. . . . . . . . . . . 12 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> ( n e. om -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) ) )
174	95, 116, 173	ralrimd 2807	. . . . . . . . . . 11 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
175	174	ralrimiv 2815	. . . . . . . . . 10 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) )
176	175	3ad2ant3 1020	. . . . . . . . 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 ) )
177		dff13 6103	. . . . . . . . 9 |- ( c : om -1-1-> A <-> ( c : om --> A /\ A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
178	115, 176, 177	sylanbrc 662	. . . . . . . 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 )
179		19.8a 1881	. . . . . . . 8 |- ( c : om -1-1-> A -> E. c c : om -1-1-> A )
180	178, 179	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 )
181	2	brdom 7486	. . . . . . 7 |- ( om ~<_ A <-> E. c c : om -1-1-> A )
182	180, 181	sylibr 212	. . . . . 6 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A )
183	182	3expib 1200	. . . . 5 |- ( A. n e. om ( b ` n ) e. B -> ( ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A ) )
184	183	exlimdv 1745	. . . 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 ) )
185	93, 184	mpd 15	. . 3 |- ( A. n e. om ( b ` n ) e. B -> om ~<_ A )
186	185	exlimiv 1743	. 2 |- ( E. b A. n e. om ( b ` n ) e. B -> om ~<_ A )
187	48, 186	syl 17	1 |- ( -. A e. Fin -> om ~<_ A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   \/ w3o 973   /\ w3a 974   = wceq 1405   E.wex 1633   e. wcel 1842   {cab 2387   =/= wne 2598   A.wral 2753   _Vcvv 3058   \ cdif 3410   C_ wss 3413   (/)c0 3737   ~Pcpw 3954   U_ciun 4270   class class class wbr 4394   |-> cmpt 4452   Ord word 4820   suc csuc 4823   dom cdm 4942   Fn wfn 5520   -->wf 5521   -1-1->wf1 5522   ` cfv 5525   omcom 6638   ~~ cen 7471   ~<_ cdom 7472   ~< csdm 7473   Fincfn 7474   cardccrd 8268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-inf2 8011  ax-cc 8767

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-om 6639  df-1st 6738  df-2nd 6739  df-recs 6999  df-rdg 7033  df-1o 7087  df-2o 7088  df-oadd 7091  df-er 7268  df-map 7379  df-en 7475  df-dom 7476  df-sdom 7477  df-fin 7478  df-card 8272  df-cda 8500

This theorem is referenced by:  domtriom  8775