Theorem domtriomlem 8715

Description: Lemma for domtriom 8716. (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 457	. . . . . . . 8 |- ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
5	4	ss2abi 3525	. . . . . . 7 |- { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
6		df-pw 3963	. . . . . . 7 |- ~P A = { y | y C_ A }
7	5, 6	sseqtr4i 3490	. . . . . 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 2535	. . . 4 |- B e. _V
10		omex 7953	. . . . 5 |- om e. _V
11	10	enref 7445	. . . 4 |- om ~~ om
12	9, 11	axcc3 8711	. . 3 |- E. b ( b Fn om /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
13		nfv 1674	. . . . . . . 8 |- F/ n -. A e. Fin
14		nfra1 2806	. . . . . . . 8 |- F/ n A. n e. om ( B =/= (/) -> ( b ` n ) e. B )
15	13, 14	nfan 1863	. . . . . . 7 |- F/ n ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) )
16		nnfi 7607	. . . . . . . . . . . . . 14 |- ( n e. om -> n e. Fin )
17		pwfi 7710	. . . . . . . . . . . . . 14 |- ( n e. Fin <-> ~P n e. Fin )
18	16, 17	sylib 196	. . . . . . . . . . . . 13 |- ( n e. om -> ~P n e. Fin )
19		ficardom 8235	. . . . . . . . . . . . 13 |- ( ~P n e. Fin -> ( card ` ~P n ) e. om )
20		isinf 7630	. . . . . . . . . . . . . 14 |- ( -. A e. Fin -> A. m e. om E. y ( y C_ A /\ y ~~ m ) )
21		breq2 4397	. . . . . . . . . . . . . . . . 17 |- ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
22	21	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
23	22	exbidv 1681	. . . . . . . . . . . . . . 15 |- ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24	23	rspcv 3168	. . . . . . . . . . . . . 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 20	. . . . . . . . . . . 12 |- ( n e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
27		finnum 8222	. . . . . . . . . . . . . . 15 |- ( ~P n e. Fin -> ~P n e. dom card )
28		cardid2 8227	. . . . . . . . . . . . . . 15 |- ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
29		entr 7464	. . . . . . . . . . . . . . . 16 |- ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
30	29	expcom 435	. . . . . . . . . . . . . . 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 565	. . . . . . . . . . . . 13 |- ( n e. om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
33	32	eximdv 1677	. . . . . . . . . . . 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 2733	. . . . . . . . . . . 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 31	. . . . . . . . 9 |- ( -. A e. Fin -> ( n e. om -> B =/= (/) ) )
40	39	adantr 465	. . . . . . . 8 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. om -> B =/= (/) ) )
41		rsp 2887	. . . . . . . . 9 |- ( A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
42	41	adantl 466	. . . . . . . 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 2818	. . . . . 6 |- ( ( -. A e. Fin /\ A. n e. om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. om ( b ` n ) e. B )
45	44	3adant2 1007	. . . . 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 1191	. . . 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 1677	. . 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 17	. 2 |- ( -. A e. Fin -> E. b A. n e. om ( b ` n ) e. B )
49		axcc2 8710	. . . . 5 |- E. c ( c Fn om /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
50		simp2 989	. . . . . . . 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 2806	. . . . . . . . . . 11 |- F/ n A. n e. om ( b ` n ) e. B
52		nfra1 2806	. . . . . . . . . . 11 |- F/ n A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
53	51, 52	nfan 1863	. . . . . . . . . 10 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
54		fvex 5802	. . . . . . . . . . . . . . . 16 |- ( b ` n ) e. _V
55		sseq1 3478	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
56		breq1 4396	. . . . . . . . . . . . . . . . 17 |- ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
57	55, 56	anbi12d 710	. . . . . . . . . . . . . . . 16 |- ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
58	54, 57, 1	elab2 3209	. . . . . . . . . . . . . . 15 |- ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
59	58	simprbi 464	. . . . . . . . . . . . . 14 |- ( ( b ` n ) e. B -> ( b ` n ) ~~ ~P n )
60	59	ralimi 2814	. . . . . . . . . . . . 13 |- ( A. n e. om ( b ` n ) e. B -> A. n e. om ( b ` n ) ~~ ~P n )
61		fveq2 5792	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ( b ` n ) = ( b ` k ) )
62		pweq 3964	. . . . . . . . . . . . . . . . 17 |- ( n = k -> ~P n = ~P k )
63	61, 62	breq12d 4406	. . . . . . . . . . . . . . . 16 |- ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
64	63	cbvralv 3046	. . . . . . . . . . . . . . 15 |- ( A. n e. om ( b ` n ) ~~ ~P n <-> A. k e. om ( b ` k ) ~~ ~P k )
65		peano2 6599	. . . . . . . . . . . . . . . . . 18 |- ( n e. om -> suc n e. om )
66		omelon 7956	. . . . . . . . . . . . . . . . . . 19 |- om e. On
67	66	onelssi 4928	. . . . . . . . . . . . . . . . . 18 |- ( suc n e. om -> suc n C_ om )
68		ssralv 3517	. . . . . . . . . . . . . . . . . 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 8477	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
71	70	ex 434	. . . . . . . . . . . . . . . . 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 7562	. . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . 14 |- ( n e. om -> ( A. n e. om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76		difss 3584	. . . . . . . . . . . . . . . . 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 5883	. . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . 15 |- ( n e. om -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
81	80	neeq1d 2725	. . . . . . . . . . . . . 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 30	. . . . . . . . . . . 12 |- ( A. n e. om ( b ` n ) e. B -> ( n e. om -> ( C ` n ) =/= (/) ) )
84	83	adantr 465	. . . . . . . . . . 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 2887	. . . . . . . . . . . 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 466	. . . . . . . . . . 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 2818	. . . . . . . . 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 1007	. . . . . . . 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 532	. . . . . . 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 1191	. . . . . 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 1677	. . . . 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 17	. . . 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 989	. . . . . . . . . 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 2806	. . . . . . . . . . . . 13 |- F/ n A. n e. om ( c ` n ) e. ( C ` n )
96	51, 95	nfan 1863	. . . . . . . . . . . 12 |- F/ n ( A. n e. om ( b ` n ) e. B /\ A. n e. om ( c ` n ) e. ( C ` n ) )
97		rsp 2887	. . . . . . . . . . . . . . . 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 2887	. . . . . . . . . . . . . . . . . 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 2521	. . . . . . . . . . . . . . . . . . 19 |- ( n e. om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
102		eldifi 3579	. . . . . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . . . . 19 |- ( ( b ` n ) e. B -> ( b ` n ) C_ A )
105	104	sseld 3456	. . . . . . . . . . . . . . . . . 18 |- ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
106	103, 105	syl9 71	. . . . . . . . . . . . . . . . 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 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 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 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 429	. . . . . . . . . . . 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 2818	. . . . . . . . . . 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 1007	. . . . . . . . . 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 5971	. . . . . . . . . 10 |- ( c : om --> A <-> ( c Fn om /\ A. n e. om ( c ` n ) e. A ) )
115	94, 113, 114	sylanbrc 664	. . . . . . . . 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 1674	. . . . . . . . . . . 12 |- F/ n k e. om
117		nnord 6587	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
118		nnord 6587	. . . . . . . . . . . . . . . 16 |- ( n e. om -> Ord n )
119		ordtri3or 4852	. . . . . . . . . . . . . . . 16 |- ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
120	117, 118, 119	syl2an 477	. . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( c ` n ) = ( c ` k ) )
124		fveq2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k = j -> ( b ` k ) = ( b ` j ) )
125	124	cbviunv 4310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
126		iuneq1 4285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
127	125, 126	syl5eq 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
128	61, 127	difeq12d 3576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
129	123, 128	eleq12d 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3169	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . . . . . . . . . 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 3579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
135		eleq1 2523	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . . 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 4314	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
141	140	sseld 3456	. . . . . . . . . . . . . . . . . . . . . 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 1186	. . . . . . . . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . . 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 3442	. . . . . . . . . . . . . . . . . . . . 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 1006	. . . . . . . . . . . . . . . . . . . 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 1187	. . . . . . . . . . . . . . . . . 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 5792	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = n -> ( b ` j ) = ( b ` n ) )
154	153	ssiun2s 4315	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
155	154	sseld 3456	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
156	102, 155	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 ) ) )
157	146, 156	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 ) ) )
158	157	3impib 1186	. . . . . . . . . . . . . . . . . . . 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 2523	. . . . . . . . . . . . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) )
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 1182	. . . . . . . . . . . . . . . . . . . 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 1187	. . . . . . . . . . . . . . . . . 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 1282	. . . . . . . . . . . . . . . . 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 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 ) ) )
170	169	3expia 1190	. . . . . . . . . . . . . . 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 41	. . . . . . . . . . . . . 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 436	. . . . . . . . . . . 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 2903	. . . . . . . . . . 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 2823	. . . . . . . . . 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 1011	. . . . . . . . 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 6073	. . . . . . . . 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 664	. . . . . . . 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 1795	. . . . . . . 8 |- ( c : om -1-1-> A -> E. c c : om -1-1-> A )
180	178, 179	syl 16	. . . . . . 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 7425	. . . . . . 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 1191	. . . . 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 1691	. . . 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 1689	. 2 |- ( E. b A. n e. om ( b ` n ) e. B -> om ~<_ A )
187	48, 186	syl 16	1 |- ( -. A e. Fin -> om ~<_ A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   \/ w3o 964   /\ w3a 965   = wceq 1370   E.wex 1587   e. wcel 1758   {cab 2436   =/= wne 2644   A.wral 2795   _Vcvv 3071   \ cdif 3426   C_ wss 3429   (/)c0 3738   ~Pcpw 3961   U_ciun 4272   class class class wbr 4393   |-> cmpt 4451   Ord word 4819   suc csuc 4822   dom cdm 4941   Fn wfn 5514   -->wf 5515   -1-1->wf1 5516   ` cfv 5519   omcom 6579   ~~ cen 7410   ~<_ cdom 7411   ~< csdm 7412   Fincfn 7413   cardccrd 8209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-inf2 7951  ax-cc 8708

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-tr 4487  df-eprel 4733  df-id 4737  df-po 4742  df-so 4743  df-fr 4780  df-we 4782  df-ord 4823  df-on 4824  df-lim 4825  df-suc 4826  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-om 6580  df-1st 6680  df-2nd 6681  df-recs 6935  df-rdg 6969  df-1o 7023  df-2o 7024  df-oadd 7027  df-er 7204  df-map 7319  df-en 7414  df-dom 7415  df-sdom 7416  df-fin 7417  df-card 8213  df-cda 8441

This theorem is referenced by:  domtriom  8716