Theorem domtriomlem 8890

Description: Lemma for domtriom 8891. (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 4584	. . . . . 6 |- ~P A e. _V
4		simpl 464	. . . . . . . 8 |- ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
5	4	ss2abi 3487	. . . . . . 7 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
6		df-pw 3944	. . . . . . 7 |- ~P A = { y | y C_ A }
7	5, 6	sseqtr4i 3451	. . . . . 6 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ ~P A
8	3, 7	ssexi 4541	. . . . 5 |- { y | ( y C_ A /\ y ~~ ~P n ) } e. _V
9	1, 8	eqeltri 2545	. . . 4 |- B e. _V
10		omex 8166	. . . . 5 |- om e. _V
11	10	enref 7620	. . . 4 |- om ~~ om
12	9, 11	axcc3 8886	. . 3 |- E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
13		nfv 1769	. . . . . . . 8 |- F/ n -. A e. Fin
14		nfra1 2785	. . . . . . . 8 |- F/ n A. n e. om ( B =/= (/) -> ( b ` n ) e. B )
15	13, 14	nfan 2031	. . . . . . 7 |- F/ n ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
16		nnfi 7783	. . . . . . . . . . . . . 14 |- ( n e. om -> n e. Fin )
17		pwfi 7887	. . . . . . . . . . . . . 14 |- ( n e. Fin <-> ~P n e. Fin )
18	16, 17	sylib 201	. . . . . . . . . . . . 13 |- ( n e. om -> ~P n e. Fin )
19		ficardom 8413	. . . . . . . . . . . . 13 |- ( ~P n e. Fin -> ( card ` ~P n ) e. om )
20		isinf 7803	. . . . . . . . . . . . . 14 |- ( -. A e. Fin -> A. m e. om E. y ( y C_ A /\ y ~~ m ) )
21		breq2 4399	. . . . . . . . . . . . . . . . 17 |- ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
22	21	anbi2d 718	. . . . . . . . . . . . . . . 16 |- ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
23	22	exbidv 1776	. . . . . . . . . . . . . . 15 |- ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24	23	rspcv 3132	. . . . . . . . . . . . . 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 32	. . . . . . . . . . . . 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 8400	. . . . . . . . . . . . . . 15 |- ( ~P n e. Fin -> ~P n e. dom card )
28		cardid2 8405	. . . . . . . . . . . . . . 15 |- ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
29		entr 7639	. . . . . . . . . . . . . . . 16 |- ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
30	29	expcom 442	. . . . . . . . . . . . . . 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 575	. . . . . . . . . . . . 13 |- ( n e. om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
33	32	eximdv 1772	. . . . . . . . . . . 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 44	. . . . . . . . . . 11 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
35	1	neeq1i 2707	. . . . . . . . . . . 12 |- ( B =/= (/) <-> { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) )
36		abn0 3754	. . . . . . . . . . . 12 |- ( { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
37	35, 36	bitri 257	. . . . . . . . . . 11 |- ( B =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
38	34, 37	syl6ibr 235	. . . . . . . . . 10 |- ( n e. om -> ( -. A e. Fin -> B =/= (/) ) )
39	38	com12 31	. . . . . . . . 9 |- ( -. A e. Fin -> ( n e. om -> B =/= (/) ) )
40	39	adantr 472	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> B =/= (/) ) )
41		rsp 2773	. . . . . . . . 9 |- ( A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
42	41	adantl 473	. . . . . . . 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 40	. . . . . . 7 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> ( b ` n ) e. B ) )
44	15, 43	ralrimi 2800	. . . . . 6 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
45	44	3adant2 1049	. . . . 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 1234	. . . 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 1772	. . 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 20	. 2 |- ( -. A e. Fin -> E. b A. n e. om ( b ` n ) e. B )
49		axcc2 8885	. . . . 5 |- E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
50		simp2 1031	. . . . . . . 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 2785	. . . . . . . . . . 11 |- F/ n A. n e. om ( b ` n ) e. B
52		nfra1 2785	. . . . . . . . . . 11 |- F/ n A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
53	51, 52	nfan 2031	. . . . . . . . . 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 3439	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
56		breq1 4398	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
57	55, 56	anbi12d 725	. . . . . . . . . . . . . . . 16 |- ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
58	54, 57, 1	elab2 3176	. . . . . . . . . . . . . . 15 |- ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
59	58	simprbi 471	. . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( b ` n ) = ( b ` k ) )
62		pweq 3945	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ~P n = ~P k )
63	61, 62	breq12d 4408	. . . . . . . . . . . . . . . 16 |- ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
64	63	cbvralv 3005	. . . . . . . . . . . . . . 15 |- ( A. n e. om ( b ` n ) ~~ ~P n <-> A. k e. om ( b ` k ) ~~ ~P k )
65		peano2 6732	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> suc n e. om )
66		omelon 8169	. . . . . . . . . . . . . . . . . . 19 |- om e. On
67	66	onelssi 5538	. . . . . . . . . . . . . . . . . 18 |- ( suc n e. om -> suc n C_ om )
68		ssralv 3479	. . . . . . . . . . . . . . . . . 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 8652	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
71	70	ex 441	. . . . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
73		sdomdif 7738	. . . . . . . . . . . . . . . 16 |- ( U_ k e. n ( b ` k ) ~< ( b ` n ) -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) )
74	72, 73	syl6 33	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
75	64, 74	syl5bi 225	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76		difss 3549	. . . . . . . . . . . . . . . . 17 |- ( ( b ` n ) \ U_ k e. n ( b ` k ) ) C_ ( b ` n )
77	54, 76	ssexi 4541	. . . . . . . . . . . . . . . 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 5972	. . . . . . . . . . . . . . . 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 685	. . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . 13 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( C ` n ) =/= (/) ) )
83	60, 82	syl5com 30	. . . . . . . . . . . 12 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( C ` n ) =/= (/) ) )
84	83	adantr 472	. . . . . . . . . . 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 2773	. . . . . . . . . . . 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 473	. . . . . . . . . . 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 40	. . . . . . . . . 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 2800	. . . . . . . . 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 1049	. . . . . . . 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 541	. . . . . . 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 1234	. . . . . 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 1772	. . . . 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 20	. . . 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 1031	. . . . . . . . . 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 2785	. . . . . . . . . . . . 13 |- F/ n A. n e. om ( c ` n ) e. ( C ` n )
96	51, 95	nfan 2031	. . . . . . . . . . . 12 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) )
97		rsp 2773	. . . . . . . . . . . . . . . 16 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( C ` n ) ) )
98	97	com12 31	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( C ` n ) ) )
99		rsp 2773	. . . . . . . . . . . . . . . . . 18 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( b ` n ) e. B ) )
100	99	com12 31	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( b ` n ) e. B ) )
101	80	eleq2d 2534	. . . . . . . . . . . . . . . . . . 19 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
102		eldifi 3544	. . . . . . . . . . . . . . . . . . 19 |- ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. ( b ` n ) )
103	101, 102	syl6bi 236	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` n ) ) )
104	58	simplbi 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( b ` n ) e. B -> ( b ` n ) C_ A )
105	104	sseld 3417	. . . . . . . . . . . . . . . . . 18 |- ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
106	103, 105	syl9 72	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
107	100, 106	syld 44	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
108	107	com23 80	. . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . 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 82	. . . . . . . . . . . . 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 436	. . . . . . . . . . . 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 2800	. . . . . . . . . . 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 1049	. . . . . . . . . 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 6064	. . . . . . . . . 10 |- ( c : om --> A <-> ( c Fn om /\ A. n e. om ( c ` n ) e. A ) )
115	94, 113, 114	sylanbrc 677	. . . . . . . . 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 1769	. . . . . . . . . . . 12 |- F/ n k e. om
117		nnord 6719	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
118		nnord 6719	. . . . . . . . . . . . . . . 16 |- ( n e. om -> Ord n )
119		ordtri3or 5462	. . . . . . . . . . . . . . . 16 |- ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
120	117, 118, 119	syl2an 485	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ n e. om ) -> ( k e. n \/ k = n \/ n e. k ) )
121	97, 101	mpbidi 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 4308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
126		iuneq1 4283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
127	125, 126	syl5eq 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
128	61, 127	difeq12d 3541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
129	123, 128	eleq12d 2543	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 31	. . . . . . . . . . . . . . . . . . . . . . . . 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 1051	. . . . . . . . . . . . . . . . . . . . . . . 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 3544	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
135		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( b ` k ) <-> ( c ` n ) e. ( b ` k ) ) )
136	134, 135	syl5ib 227	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
137	136	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . . . . . . . . . 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 4312	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
141	140	sseld 3417	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. n -> ( ( c ` n ) e. ( b ` k ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
142	139, 141	syl5 32	. . . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . . 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 31	. . . . . . . . . . . . . . . . . . . . . . . 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 1052	. . . . . . . . . . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . . . . . . . . . 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 3403	. . . . . . . . . . . . . . . . . . . . 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 1048	. . . . . . . . . . . . . . . . . . . 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 179	. . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . 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 27	. . . . . . . . . . . . . . . . . 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 4313	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
154	153	sseld 3417	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
155	102, 154	syl5 32	. . . . . . . . . . . . . . . . . . . . . 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 32	. . . . . . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . . . . . . . . . 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 3545	. . . . . . . . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . . . . . . . . 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 1053	. . . . . . . . . . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . . . . . . . . . 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 1224	. . . . . . . . . . . . . . . . . . . 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 179	. . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . 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 1357	. . . . . . . . . . . . . . . . 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 31	. . . . . . . . . . . . . . . 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 1233	. . . . . . . . . . . . . . 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 41	. . . . . . . . . . . . . 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 81	. . . . . . . . . . . . 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 443	. . . . . . . . . . . 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 2802	. . . . . . . . . . 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 2808	. . . . . . . . . 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 1053	. . . . . . . . 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 6177	. . . . . . . . 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 677	. . . . . . . 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 1955	. . . . . . . 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 7599	. . . . . . 7 |- ( om ~<_ A <-> E. c c : om -1-1-> A )
181	179, 180	sylibr 217	. . . . . 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 1234	. . . . 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 1787	. . . 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 1784	. 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 376   \/ w3o 1006   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   {cab 2457   =/= wne 2641   A.wral 2756   _Vcvv 3031   \ cdif 3387   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   U_ciun 4269   class class class wbr 4395   |-> cmpt 4454   dom cdm 4839   Ord word 5429   suc csuc 5432   Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   ` cfv 5589   omcom 6711   ~~ cen 7584   ~<_ cdom 7585   ~< csdm 7586   Fincfn 7587   cardccrd 8387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cc 8883

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616

This theorem is referenced by:  domtriom  8891