Theorem domtriomlem 9264

Description: Lemma for domtriom 9265. (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 4848	. . . . . 6 |- ~P A e. _V
4		simpl 473	. . . . . . . 8 |- ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
5	4	ss2abi 3674	. . . . . . 7 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
6		df-pw 4160	. . . . . . 7 |- ~P A = { y | y C_ A }
7	5, 6	sseqtr4i 3638	. . . . . 6 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ ~P A
8	3, 7	ssexi 4803	. . . . 5 |- { y | ( y C_ A /\ y ~~ ~P n ) } e. _V
9	1, 8	eqeltri 2697	. . . 4 |- B e. _V
10		omex 8540	. . . . 5 |- om e. _V
11	10	enref 7988	. . . 4 |- om ~~ om
12	9, 11	axcc3 9260	. . 3 |- E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
13		nfv 1843	. . . . . . . 8 |- F/ n -. A e. Fin
14		nfra1 2941	. . . . . . . 8 |- F/ n A. n e. om ( B =/= (/) -> ( b ` n ) e. B )
15	13, 14	nfan 1828	. . . . . . 7 |- F/ n ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
16		nnfi 8153	. . . . . . . . . . . . . 14 |- ( n e. om -> n e. Fin )
17		pwfi 8261	. . . . . . . . . . . . . 14 |- ( n e. Fin <-> ~P n e. Fin )
18	16, 17	sylib 208	. . . . . . . . . . . . 13 |- ( n e. om -> ~P n e. Fin )
19		ficardom 8787	. . . . . . . . . . . . 13 |- ( ~P n e. Fin -> ( card ` ~P n ) e. om )
20		isinf 8173	. . . . . . . . . . . . . 14 |- ( -. A e. Fin -> A. m e. om E. y ( y C_ A /\ y ~~ m ) )
21		breq2 4657	. . . . . . . . . . . . . . . . 17 |- ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
22	21	anbi2d 740	. . . . . . . . . . . . . . . 16 |- ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
23	22	exbidv 1850	. . . . . . . . . . . . . . 15 |- ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24	23	rspcv 3305	. . . . . . . . . . . . . 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 8774	. . . . . . . . . . . . . . 15 |- ( ~P n e. Fin -> ~P n e. dom card )
28		cardid2 8779	. . . . . . . . . . . . . . 15 |- ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
29		entr 8008	. . . . . . . . . . . . . . . 16 |- ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
30	29	expcom 451	. . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 13 |- ( n e. om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
33	32	eximdv 1846	. . . . . . . . . . . 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 47	. . . . . . . . . . 11 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
35	1	neeq1i 2858	. . . . . . . . . . . 12 |- ( B =/= (/) <-> { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) )
36		abn0 3954	. . . . . . . . . . . 12 |- ( { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
37	35, 36	bitri 264	. . . . . . . . . . 11 |- ( B =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
38	34, 37	syl6ibr 242	. . . . . . . . . 10 |- ( n e. om -> ( -. A e. Fin -> B =/= (/) ) )
39	38	com12 32	. . . . . . . . 9 |- ( -. A e. Fin -> ( n e. om -> B =/= (/) ) )
40	39	adantr 481	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> B =/= (/) ) )
41		rsp 2929	. . . . . . . . 9 |- ( A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
42	41	adantl 482	. . . . . . . 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 43	. . . . . . 7 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> ( b ` n ) e. B ) )
44	15, 43	ralrimi 2957	. . . . . 6 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
45	44	3adant2 1080	. . . . 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 1268	. . . 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 1846	. . 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 9259	. . . . 5 |- E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
50		simp2 1062	. . . . . . . 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 2941	. . . . . . . . . . 11 |- F/ n A. n e. om ( b ` n ) e. B
52		nfra1 2941	. . . . . . . . . . 11 |- F/ n A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
53	51, 52	nfan 1828	. . . . . . . . . 10 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
54		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( b ` n ) e. _V
55		sseq1 3626	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
56		breq1 4656	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
57	55, 56	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
58	54, 57, 1	elab2 3354	. . . . . . . . . . . . . . 15 |- ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
59	58	simprbi 480	. . . . . . . . . . . . . 14 |- ( ( b ` n ) e. B -> ( b ` n ) ~~ ~P n )
60	59	ralimi 2952	. . . . . . . . . . . . 13 |- ( A. n e. om ( b ` n ) e. B -> A. n e. om ( b ` n ) ~~ ~P n )
61		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( b ` n ) = ( b ` k ) )
62		pweq 4161	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ~P n = ~P k )
63	61, 62	breq12d 4666	. . . . . . . . . . . . . . . 16 |- ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
64	63	cbvralv 3171	. . . . . . . . . . . . . . 15 |- ( A. n e. om ( b ` n ) ~~ ~P n <-> A. k e. om ( b ` k ) ~~ ~P k )
65		peano2 7086	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> suc n e. om )
66		omelon 8543	. . . . . . . . . . . . . . . . . . 19 |- om e. On
67	66	onelssi 5836	. . . . . . . . . . . . . . . . . 18 |- ( suc n e. om -> suc n C_ om )
68		ssralv 3666	. . . . . . . . . . . . . . . . . 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 9026	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
71	70	ex 450	. . . . . . . . . . . . . . . . 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 47	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. k e. om ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
73		sdomdif 8108	. . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76		difss 3737	. . . . . . . . . . . . . . . . 17 |- ( ( b ` n ) \ U_ k e. n ( b ` k ) ) C_ ( b ` n )
77	54, 76	ssexi 4803	. . . . . . . . . . . . . . . 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 6291	. . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
81	80	neeq1d 2853	. . . . . . . . . . . . . 14 |- ( n e. om -> ( ( C ` n ) =/= (/) <-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
82	75, 81	sylibrd 249	. . . . . . . . . . . . 13 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( C ` n ) =/= (/) ) )
83	60, 82	syl5com 31	. . . . . . . . . . . 12 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( C ` n ) =/= (/) ) )
84	83	adantr 481	. . . . . . . . . . 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 2929	. . . . . . . . . . . 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 482	. . . . . . . . . . 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 43	. . . . . . . . . 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 2957	. . . . . . . . 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 1080	. . . . . . . 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 554	. . . . . . 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 1268	. . . . . 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 1846	. . . . 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 1062	. . . . . . . . . 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 2941	. . . . . . . . . . . . 13 |- F/ n A. n e. om ( c ` n ) e. ( C ` n )
96	51, 95	nfan 1828	. . . . . . . . . . . 12 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) )
97		rsp 2929	. . . . . . . . . . . . . . . 16 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( C ` n ) ) )
98	97	com12 32	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( C ` n ) ) )
99		rsp 2929	. . . . . . . . . . . . . . . . . 18 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( b ` n ) e. B ) )
100	99	com12 32	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( b ` n ) e. B ) )
101	80	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
102		eldifi 3732	. . . . . . . . . . . . . . . . . . 19 |- ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. ( b ` n ) )
103	101, 102	syl6bi 243	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` n ) ) )
104	58	simplbi 476	. . . . . . . . . . . . . . . . . . 19 |- ( ( b ` n ) e. B -> ( b ` n ) C_ A )
105	104	sseld 3602	. . . . . . . . . . . . . . . . . 18 |- ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
106	103, 105	syl9 77	. . . . . . . . . . . . . . . . 17 |- ( n e. om -> ( ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
107	100, 106	syld 47	. . . . . . . . . . . . . . . 16 |- ( n e. om -> ( A. n e. om ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
108	107	com23 86	. . . . . . . . . . . . . . 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 47	. . . . . . . . . . . . . 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 88	. . . . . . . . . . . . 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 445	. . . . . . . . . . . 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 2957	. . . . . . . . . . 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 1080	. . . . . . . . . 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 6388	. . . . . . . . . 10 |- ( c : om --> A <-> ( c Fn om /\ A. n e. om ( c ` n ) e. A ) )
115	94, 113, 114	sylanbrc 698	. . . . . . . . 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 1843	. . . . . . . . . . . 12 |- F/ n k e. om
117		nnord 7073	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
118		nnord 7073	. . . . . . . . . . . . . . . 16 |- ( n e. om -> Ord n )
119		ordtri3or 5755	. . . . . . . . . . . . . . . 16 |- ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
120	117, 118, 119	syl2an 494	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ n e. om ) -> ( k e. n \/ k = n \/ n e. k ) )
121		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( n = k -> ( c ` n ) = ( c ` k ) )
122		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k = j -> ( b ` k ) = ( b ` j ) )
123	122	cbviunv 4559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
124		iuneq1 4534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
125	123, 124	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
126	61, 125	difeq12d 3729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
127	121, 126	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n = k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) <-> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
128	127	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 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 ) ) ) )
129	97, 101	mpbidi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( n e. om -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
130	95, 129	ralrimi 2957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> A. n e. om ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
131	128, 130	syl11 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 ) ) ) )
132	131	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
133		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
134		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( b ` k ) <-> ( c ` n ) e. ( b ` k ) ) )
135	133, 134	syl5ib 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
136	135	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
137	132, 136	syld 47	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
138	137	imp 445	. . . . . . . . . . . . . . . . . . . . . 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 ) )
139		ssiun2 4563	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
140	139	sseld 3602	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. n -> ( ( c ` n ) e. ( b ` k ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
141	138, 140	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 ) ) )
142	141	3impib 1262	. . . . . . . . . . . . . . . . . . . 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 ) )
143	129	com12 32	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. om -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
144	143	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
145	144	imp 445	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
146	145	eldifbd 3587	. . . . . . . . . . . . . . . . . . . . 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 ) )
147	146	3adant1 1079	. . . . . . . . . . . . . . . . . . . 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 ) )
148	142, 147	pm2.21dd 186	. . . . . . . . . . . . . . . . . . 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 )
149	148	3exp 1264	. . . . . . . . . . . . . . . . . 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 ) ) )
150		2a1 28	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( ( k e. om /\ n e. om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
151		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = n -> ( b ` j ) = ( b ` n ) )
152	151	ssiun2s 4564	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
153	152	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
154	102, 153	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 ) ) )
155	145, 154	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 ) ) )
156	155	3impib 1262	. . . . . . . . . . . . . . . . . . . 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 ) )
157		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
158		eldifn 3733	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( c ` n ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) )
159	157, 158	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
160	159	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
161	132, 160	syld 47	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
162	161	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 ) ) ) )
163	162	3imp 1256	. . . . . . . . . . . . . . . . . . . 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 ) )
164	156, 163	pm2.21dd 186	. . . . . . . . . . . . . . . . . . 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 )
165	164	3exp 1264	. . . . . . . . . . . . . . . . . 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 ) ) )
166	149, 150, 165	3jaoi 1391	. . . . . . . . . . . . . . . . 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 ) ) )
167	166	com12 32	. . . . . . . . . . . . . . . 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 ) ) )
168	167	3expia 1267	. . . . . . . . . . . . . . 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 ) ) ) )
169	120, 168	mpid 44	. . . . . . . . . . . . . 14 |- ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> ( A. n e. om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
170	169	com3r 87	. . . . . . . . . . . . 13 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( ( k e. om /\ n e. om ) -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
171	170	expd 452	. . . . . . . . . . . 12 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> ( n e. om -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) ) )
172	95, 116, 171	ralrimd 2959	. . . . . . . . . . 11 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> ( k e. om -> A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
173	172	ralrimiv 2965	. . . . . . . . . 10 |- ( A. n e. om ( c ` n ) e. ( C ` n ) -> A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) )
174	173	3ad2ant3 1084	. . . . . . . . 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 ) )
175		dff13 6512	. . . . . . . . 9 |- ( c : om -1-1-> A <-> ( c : om --> A /\ A. k e. om A. n e. om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
176	115, 174, 175	sylanbrc 698	. . . . . . . 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 )
177		19.8a 2052	. . . . . . . 8 |- ( c : om -1-1-> A -> E. c c : om -1-1-> A )
178	176, 177	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 )
179	2	brdom 7967	. . . . . . 7 |- ( om ~<_ A <-> E. c c : om -1-1-> A )
180	178, 179	sylibr 224	. . . . . 6 |- ( ( A. n e. om ( b ` n ) e. B /\ c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A )
181	180	3expib 1268	. . . . 5 |- ( A. n e. om ( b ` n ) e. B -> ( ( c Fn om /\ A. n e. om ( c ` n ) e. ( C ` n ) ) -> om ~<_ A ) )
182	181	exlimdv 1861	. . . 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 ) )
183	93, 182	mpd 15	. . 3 |- ( A. n e. om ( b ` n ) e. B -> om ~<_ A )
184	183	exlimiv 1858	. 2 |- ( E. b A. n e. om ( b ` n ) e. B -> om ~<_ A )
185	48, 184	syl 17	1 |- ( -. A e. Fin -> om ~<_ A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   Ord word 5722   suc csuc 5725   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   ` cfv 5888   omcom 7065   ~~ cen 7952   ~<_ cdom 7953   ~< csdm 7954   Fincfn 7955   cardccrd 8761

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990

This theorem is referenced by:  domtriom  9265