Metamath Proof Explorer

Theorem domtriomlem

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

Ref Expression
Hypotheses 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 domtriomlem 
|- ( -. A e. Fin -> _om ~<_ A )

Proof

Step Hyp Ref Expression
1 domtriomlem.1 
 |-  A e. _V
2 domtriomlem.2 
 |-  B = { y | ( y C_ A /\ y ~~ ~P n ) }
3 domtriomlem.3 
 |-  C = ( n e. _om |-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
4 1 pwex 
 |-  ~P A e. _V
5 simpl 
 |-  ( ( y C_ A /\ y ~~ ~P n ) -> y C_ A )
6 5 ss2abi 
 |-  { y | ( y C_ A /\ y ~~ ~P n ) } C_ { y | y C_ A }
7 df-pw 
 |-  ~P A = { y | y C_ A }
8 6 7 sseqtrri 
 |-  { y | ( y C_ A /\ y ~~ ~P n ) } C_ ~P A
9 4 8 ssexi 
 |-  { y | ( y C_ A /\ y ~~ ~P n ) } e. _V
10 2 9 eqeltri 
 |-  B e. _V
11 omex 
 |-  _om e. _V
12 11 enref 
 |-  _om ~~ _om
13 10 12 axcc3 
 |-  E. b ( b Fn _om /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) )
14 nfv 
 |-  F/ n -. A e. Fin
15 nfra1 
 |-  F/ n A. n e. _om ( B =/= (/) -> ( b ` n ) e. B )
16 14 15 nfan 
 |-  F/ n ( -. A e. Fin /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) )
17 nnfi 
 |-  ( n e. _om -> n e. Fin )
18 pwfi 
 |-  ( n e. Fin <-> ~P n e. Fin )
19 17 18 sylib 
 |-  ( n e. _om -> ~P n e. Fin )
20 ficardom 
 |-  ( ~P n e. Fin -> ( card ` ~P n ) e. _om )
21 isinf 
 |-  ( -. A e. Fin -> A. m e. _om E. y ( y C_ A /\ y ~~ m ) )
22 breq2 
 |-  ( m = ( card ` ~P n ) -> ( y ~~ m <-> y ~~ ( card ` ~P n ) ) )
23 22 anbi2d 
 |-  ( m = ( card ` ~P n ) -> ( ( y C_ A /\ y ~~ m ) <-> ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
24 23 exbidv 
 |-  ( m = ( card ` ~P n ) -> ( E. y ( y C_ A /\ y ~~ m ) <-> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
25 24 rspcv 
 |-  ( ( 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 ) ) ) )
26 21 25 syl5 
 |-  ( ( card ` ~P n ) e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
27 19 20 26 3syl 
 |-  ( n e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) ) )
28 finnum 
 |-  ( ~P n e. Fin -> ~P n e. dom card )
29 cardid2 
 |-  ( ~P n e. dom card -> ( card ` ~P n ) ~~ ~P n )
30 entr 
 |-  ( ( y ~~ ( card ` ~P n ) /\ ( card ` ~P n ) ~~ ~P n ) -> y ~~ ~P n )
31 30 expcom 
 |-  ( ( card ` ~P n ) ~~ ~P n -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
32 19 28 29 31 4syl 
 |-  ( n e. _om -> ( y ~~ ( card ` ~P n ) -> y ~~ ~P n ) )
33 32 anim2d 
 |-  ( n e. _om -> ( ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> ( y C_ A /\ y ~~ ~P n ) ) )
34 33 eximdv 
 |-  ( n e. _om -> ( E. y ( y C_ A /\ y ~~ ( card ` ~P n ) ) -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
35 27 34 syld 
 |-  ( n e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ ~P n ) ) )
36 2 neeq1i 
 |-  ( B =/= (/) <-> { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) )
37 abn0 
 |-  ( { y | ( y C_ A /\ y ~~ ~P n ) } =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
38 36 37 bitri 
 |-  ( B =/= (/) <-> E. y ( y C_ A /\ y ~~ ~P n ) )
39 35 38 imbitrrdi 
 |-  ( n e. _om -> ( -. A e. Fin -> B =/= (/) ) )
40 39 com12 
 |-  ( -. A e. Fin -> ( n e. _om -> B =/= (/) ) )
41 40 adantr 
 |-  ( ( -. A e. Fin /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. _om -> B =/= (/) ) )
42 rsp 
 |-  ( A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) -> ( n e. _om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
43 42 adantl 
 |-  ( ( -. A e. Fin /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. _om -> ( B =/= (/) -> ( b ` n ) e. B ) ) )
44 41 43 mpdd 
 |-  ( ( -. A e. Fin /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) ) -> ( n e. _om -> ( b ` n ) e. B ) )
45 16 44 ralrimi 
 |-  ( ( -. A e. Fin /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. _om ( b ` n ) e. B )
46 45 3adant2 
 |-  ( ( -. 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 3expib 
 |-  ( -. A e. Fin -> ( ( b Fn _om /\ A. n e. _om ( B =/= (/) -> ( b ` n ) e. B ) ) -> A. n e. _om ( b ` n ) e. B ) )
48 47 eximdv 
 |-  ( -. 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 ) )
49 13 48 mpi 
 |-  ( -. A e. Fin -> E. b A. n e. _om ( b ` n ) e. B )
50 axcc2 
 |-  E. c ( c Fn _om /\ A. n e. _om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
51 simp2 
 |-  ( ( 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 )
52 nfra1 
 |-  F/ n A. n e. _om ( b ` n ) e. B
53 nfra1 
 |-  F/ n A. n e. _om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) )
54 52 53 nfan 
 |-  F/ n ( A. n e. _om ( b ` n ) e. B /\ A. n e. _om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) )
55 fvex 
 |-  ( b ` n ) e. _V
56 sseq1 
 |-  ( y = ( b ` n ) -> ( y C_ A <-> ( b ` n ) C_ A ) )
57 breq1 
 |-  ( y = ( b ` n ) -> ( y ~~ ~P n <-> ( b ` n ) ~~ ~P n ) )
58 56 57 anbi12d 
 |-  ( y = ( b ` n ) -> ( ( y C_ A /\ y ~~ ~P n ) <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) ) )
59 55 58 2 elab2 
 |-  ( ( b ` n ) e. B <-> ( ( b ` n ) C_ A /\ ( b ` n ) ~~ ~P n ) )
60 59 simprbi 
 |-  ( ( b ` n ) e. B -> ( b ` n ) ~~ ~P n )
61 60 ralimi 
 |-  ( A. n e. _om ( b ` n ) e. B -> A. n e. _om ( b ` n ) ~~ ~P n )
62 fveq2 
 |-  ( n = k -> ( b ` n ) = ( b ` k ) )
63 pweq 
 |-  ( n = k -> ~P n = ~P k )
64 62 63 breq12d 
 |-  ( n = k -> ( ( b ` n ) ~~ ~P n <-> ( b ` k ) ~~ ~P k ) )
65 64 cbvralvw 
 |-  ( A. n e. _om ( b ` n ) ~~ ~P n <-> A. k e. _om ( b ` k ) ~~ ~P k )
66 peano2 
 |-  ( n e. _om -> suc n e. _om )
67 omelon 
 |-  _om e. On
68 67 onelssi 
 |-  ( suc n e. _om -> suc n C_ _om )
69 ssralv 
 |-  ( suc n C_ _om -> ( A. k e. _om ( b ` k ) ~~ ~P k -> A. k e. suc n ( b ` k ) ~~ ~P k ) )
70 66 68 69 3syl 
 |-  ( n e. _om -> ( A. k e. _om ( b ` k ) ~~ ~P k -> A. k e. suc n ( b ` k ) ~~ ~P k ) )
71 pwsdompw 
 |-  ( ( n e. _om /\ A. k e. suc n ( b ` k ) ~~ ~P k ) -> U_ k e. n ( b ` k ) ~< ( b ` n ) )
72 71 ex 
 |-  ( n e. _om -> ( A. k e. suc n ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
73 70 72 syld 
 |-  ( n e. _om -> ( A. k e. _om ( b ` k ) ~~ ~P k -> U_ k e. n ( b ` k ) ~< ( b ` n ) ) )
74 sdomdif 
 |-  ( U_ k e. n ( b ` k ) ~< ( b ` n ) -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) )
75 73 74 syl6 
 |-  ( n e. _om -> ( A. k e. _om ( b ` k ) ~~ ~P k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
76 65 75 biimtrid 
 |-  ( n e. _om -> ( A. n e. _om ( b ` n ) ~~ ~P n -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
77 55 difexi 
 |-  ( ( b ` n ) \ U_ k e. n ( b ` k ) ) e. _V
78 3 fvmpt2 
 |-  ( ( n e. _om /\ ( ( b ` n ) \ U_ k e. n ( b ` k ) ) e. _V ) -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
79 77 78 mpan2 
 |-  ( n e. _om -> ( C ` n ) = ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
80 79 neeq1d 
 |-  ( n e. _om -> ( ( C ` n ) =/= (/) <-> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) =/= (/) ) )
81 76 80 sylibrd 
 |-  ( n e. _om -> ( A. n e. _om ( b ` n ) ~~ ~P n -> ( C ` n ) =/= (/) ) )
82 61 81 syl5com 
 |-  ( A. n e. _om ( b ` n ) e. B -> ( n e. _om -> ( C ` n ) =/= (/) ) )
83 82 adantr 
 |-  ( ( A. n e. _om ( b ` n ) e. B /\ A. n e. _om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) -> ( n e. _om -> ( C ` n ) =/= (/) ) )
84 rsp 
 |-  ( A. n e. _om ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) -> ( n e. _om -> ( ( C ` n ) =/= (/) -> ( c ` n ) e. ( C ` n ) ) ) )
85 84 adantl 
 |-  ( ( 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 ) ) ) )
86 83 85 mpdd 
 |-  ( ( 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 ) ) )
87 54 86 ralrimi 
 |-  ( ( 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 ) )
88 87 3adant2 
 |-  ( ( 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 ) )
89 51 88 jca 
 |-  ( ( 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 ) ) )
90 89 3expib 
 |-  ( 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 eximdv 
 |-  ( 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 ) ) ) )
92 50 91 mpi 
 |-  ( A. n e. _om ( b ` n ) e. B -> E. c ( c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) )
93 simp2 
 |-  ( ( A. n e. _om ( b ` n ) e. B /\ c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> c Fn _om )
94 nfra1 
 |-  F/ n A. n e. _om ( c ` n ) e. ( C ` n )
95 52 94 nfan 
 |-  F/ n ( A. n e. _om ( b ` n ) e. B /\ A. n e. _om ( c ` n ) e. ( C ` n ) )
96 rsp 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( n e. _om -> ( c ` n ) e. ( C ` n ) ) )
97 96 com12 
 |-  ( n e. _om -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( C ` n ) ) )
98 rsp 
 |-  ( A. n e. _om ( b ` n ) e. B -> ( n e. _om -> ( b ` n ) e. B ) )
99 98 com12 
 |-  ( n e. _om -> ( A. n e. _om ( b ` n ) e. B -> ( b ` n ) e. B ) )
100 79 eleq2d 
 |-  ( n e. _om -> ( ( c ` n ) e. ( C ` n ) <-> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
101 eldifi 
 |-  ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. ( b ` n ) )
102 100 101 biimtrdi 
 |-  ( n e. _om -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` n ) ) )
103 59 simplbi 
 |-  ( ( b ` n ) e. B -> ( b ` n ) C_ A )
104 103 sseld 
 |-  ( ( b ` n ) e. B -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. A ) )
105 102 104 syl9 
 |-  ( n e. _om -> ( ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
106 99 105 syld 
 |-  ( n e. _om -> ( A. n e. _om ( b ` n ) e. B -> ( ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. A ) ) )
107 106 com23 
 |-  ( n e. _om -> ( ( c ` n ) e. ( C ` n ) -> ( A. n e. _om ( b ` n ) e. B -> ( c ` n ) e. A ) ) )
108 97 107 syld 
 |-  ( n e. _om -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( A. n e. _om ( b ` n ) e. B -> ( c ` n ) e. A ) ) )
109 108 com13 
 |-  ( A. n e. _om ( b ` n ) e. B -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( n e. _om -> ( c ` n ) e. A ) ) )
110 109 imp 
 |-  ( ( 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 95 110 ralrimi 
 |-  ( ( 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 )
112 111 3adant2 
 |-  ( ( 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 )
113 ffnfv 
 |-  ( c : _om --> A <-> ( c Fn _om /\ A. n e. _om ( c ` n ) e. A ) )
114 93 112 113 sylanbrc 
 |-  ( ( A. n e. _om ( b ` n ) e. B /\ c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> c : _om --> A )
115 nfv 
 |-  F/ n k e. _om
116 nnord 
 |-  ( k e. _om -> Ord k )
117 nnord 
 |-  ( n e. _om -> Ord n )
118 ordtri3or 
 |-  ( ( Ord k /\ Ord n ) -> ( k e. n \/ k = n \/ n e. k ) )
119 116 117 118 syl2an 
 |-  ( ( k e. _om /\ n e. _om ) -> ( k e. n \/ k = n \/ n e. k ) )
120 fveq2 
 |-  ( n = k -> ( c ` n ) = ( c ` k ) )
121 fveq2 
 |-  ( k = j -> ( b ` k ) = ( b ` j ) )
122 121 cbviunv 
 |-  U_ k e. n ( b ` k ) = U_ j e. n ( b ` j )
123 iuneq1 
 |-  ( n = k -> U_ j e. n ( b ` j ) = U_ j e. k ( b ` j ) )
124 122 123 eqtrid 
 |-  ( n = k -> U_ k e. n ( b ` k ) = U_ j e. k ( b ` j ) )
125 62 124 difeq12d 
 |-  ( n = k -> ( ( b ` n ) \ U_ k e. n ( b ` k ) ) = ( ( b ` k ) \ U_ j e. k ( b ` j ) ) )
126 120 125 eleq12d 
 |-  ( n = k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) <-> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
127 126 rspccv 
 |-  ( 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 ) ) ) )
128 96 100 mpbidi 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( n e. _om -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
129 94 128 ralrimi 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> A. n e. _om ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) )
130 127 129 syl11 
 |-  ( k e. _om -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) ) )
131 130 3ad2ant1 
 |-  ( ( 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 ) ) ) )
132 eldifi 
 |-  ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` k ) e. ( b ` k ) )
133 eleq1 
 |-  ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( b ` k ) <-> ( c ` n ) e. ( b ` k ) ) )
134 132 133 imbitrid 
 |-  ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> ( c ` n ) e. ( b ` k ) ) )
135 134 3ad2ant3 
 |-  ( ( 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 ) ) )
136 131 135 syld 
 |-  ( ( k e. _om /\ n e. _om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( b ` k ) ) )
137 136 imp 
 |-  ( ( ( 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 ssiun2 
 |-  ( k e. n -> ( b ` k ) C_ U_ k e. n ( b ` k ) )
139 138 sseld 
 |-  ( k e. n -> ( ( c ` n ) e. ( b ` k ) -> ( c ` n ) e. U_ k e. n ( b ` k ) ) )
140 137 139 syl5 
 |-  ( 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 ) ) )
141 140 3impib 
 |-  ( ( 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 128 com12 
 |-  ( n e. _om -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) ) )
143 142 3ad2ant2 
 |-  ( ( 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 ) ) ) )
144 143 imp 
 |-  ( ( ( 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 eldifbd 
 |-  ( ( ( 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 ) )
146 145 3adant1 
 |-  ( ( 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 ) )
147 141 146 pm2.21dd 
 |-  ( ( k e. n /\ ( k e. _om /\ n e. _om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> k = n )
148 147 3exp 
 |-  ( 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 2a1 
 |-  ( k = n -> ( ( k e. _om /\ n e. _om /\ ( c ` k ) = ( c ` n ) ) -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
150 fveq2 
 |-  ( j = n -> ( b ` j ) = ( b ` n ) )
151 150 ssiun2s 
 |-  ( n e. k -> ( b ` n ) C_ U_ j e. k ( b ` j ) )
152 151 sseld 
 |-  ( n e. k -> ( ( c ` n ) e. ( b ` n ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
153 101 152 syl5 
 |-  ( n e. k -> ( ( c ` n ) e. ( ( b ` n ) \ U_ k e. n ( b ` k ) ) -> ( c ` n ) e. U_ j e. k ( b ` j ) ) )
154 144 153 syl5 
 |-  ( 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 ) ) )
155 154 3impib 
 |-  ( ( 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 eleq1 
 |-  ( ( 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 ) ) ) )
157 eldifn 
 |-  ( ( c ` n ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) )
158 156 157 biimtrdi 
 |-  ( ( c ` k ) = ( c ` n ) -> ( ( c ` k ) e. ( ( b ` k ) \ U_ j e. k ( b ` j ) ) -> -. ( c ` n ) e. U_ j e. k ( b ` j ) ) )
159 158 3ad2ant3 
 |-  ( ( 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 ) ) )
160 131 159 syld 
 |-  ( ( 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 ) ) )
161 160 a1i 
 |-  ( 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 ) ) ) )
162 161 3imp 
 |-  ( ( 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 155 162 pm2.21dd 
 |-  ( ( n e. k /\ ( k e. _om /\ n e. _om /\ ( c ` k ) = ( c ` n ) ) /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> k = n )
164 163 3exp 
 |-  ( 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 148 149 164 3jaoi 
 |-  ( ( 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 ) ) )
166 165 com12 
 |-  ( ( 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 ) ) )
167 166 3expia 
 |-  ( ( 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 119 167 mpid 
 |-  ( ( k e. _om /\ n e. _om ) -> ( ( c ` k ) = ( c ` n ) -> ( A. n e. _om ( c ` n ) e. ( C ` n ) -> k = n ) ) )
169 168 com3r 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( ( k e. _om /\ n e. _om ) -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
170 169 expd 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( k e. _om -> ( n e. _om -> ( ( c ` k ) = ( c ` n ) -> k = n ) ) ) )
171 94 115 170 ralrimd 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> ( k e. _om -> A. n e. _om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
172 171 ralrimiv 
 |-  ( A. n e. _om ( c ` n ) e. ( C ` n ) -> A. k e. _om A. n e. _om ( ( c ` k ) = ( c ` n ) -> k = n ) )
173 172 3ad2ant3 
 |-  ( ( 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 ) )
174 dff13 
 |-  ( c : _om -1-1-> A <-> ( c : _om --> A /\ A. k e. _om A. n e. _om ( ( c ` k ) = ( c ` n ) -> k = n ) ) )
175 114 173 174 sylanbrc 
 |-  ( ( 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 )
176 175 19.8ad 
 |-  ( ( 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 )
177 1 brdom 
 |-  ( _om ~<_ A <-> E. c c : _om -1-1-> A )
178 176 177 sylibr 
 |-  ( ( A. n e. _om ( b ` n ) e. B /\ c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> _om ~<_ A )
179 178 3expib 
 |-  ( A. n e. _om ( b ` n ) e. B -> ( ( c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> _om ~<_ A ) )
180 179 exlimdv 
 |-  ( A. n e. _om ( b ` n ) e. B -> ( E. c ( c Fn _om /\ A. n e. _om ( c ` n ) e. ( C ` n ) ) -> _om ~<_ A ) )
181 92 180 mpd 
 |-  ( A. n e. _om ( b ` n ) e. B -> _om ~<_ A )
182 181 exlimiv 
 |-  ( E. b A. n e. _om ( b ` n ) e. B -> _om ~<_ A )
183 49 182 syl 
 |-  ( -. A e. Fin -> _om ~<_ A )