This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin1a2lem13

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2lem13 
|- ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) -> -. ( B \ C ) e. Fin2 )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> ( B \ C ) e. Fin2 )
2 simpll1 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> A C_ ~P B )
3 ssel2 
 |-  ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4 3 elpwid 
 |-  ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5 4 ssdifd 
 |-  ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6 sseq1 
 |-  ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7 5 6 syl5ibrcom 
 |-  ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8 7 rexlimdva 
 |-  ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9 eqid 
 |-  ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
10 9 elrnmpt 
 |-  ( f e. _V -> ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) ) )
11 10 elv 
 |-  ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) )
12 velpw 
 |-  ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
13 8 11 12 3imtr4g 
 |-  ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
14 13 ssrdv 
 |-  ( A C_ ~P B -> ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) )
15 2 14 syl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) )
16 simplrr 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> C e. A )
17 difid 
 |-  ( C \ C ) = (/)
18 17 eqcomi 
 |-  (/) = ( C \ C )
19 difeq1 
 |-  ( g = C -> ( g \ C ) = ( C \ C ) )
20 19 rspceeqv 
 |-  ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
21 18 20 mpan2 
 |-  ( C e. A -> E. g e. A (/) = ( g \ C ) )
22 0ex 
 |-  (/) e. _V
23 9 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) ) )
24 22 23 ax-mp 
 |-  ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) )
25 21 24 sylibr 
 |-  ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
26 ne0i 
 |-  ( (/) e. ran ( g e. A |-> ( g \ C ) ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
27 16 25 26 3syl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
28 simpll2 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> [C.] Or A )
29 9 elrnmpt 
 |-  ( x e. _V -> ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) ) )
30 29 elv 
 |-  ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) )
31 difeq1 
 |-  ( g = e -> ( g \ C ) = ( e \ C ) )
32 31 eqeq2d 
 |-  ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
33 32 cbvrexvw 
 |-  ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
34 sorpssi 
 |-  ( ( [C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
35 ssdif 
 |-  ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
36 ssdif 
 |-  ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
37 35 36 orim12i 
 |-  ( ( e C_ g \/ g C_ e ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
38 34 37 syl 
 |-  ( ( [C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
39 sseq2 
 |-  ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
40 sseq1 
 |-  ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
41 39 40 orbi12d 
 |-  ( f = ( g \ C ) -> ( ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) <-> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) ) )
42 38 41 syl5ibrcom 
 |-  ( ( [C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
43 42 expr 
 |-  ( ( [C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
44 43 rexlimdv 
 |-  ( ( [C.] Or A /\ e e. A ) -> ( E. g e. A f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
45 11 44 biimtrid 
 |-  ( ( [C.] Or A /\ e e. A ) -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46 45 ralrimiv 
 |-  ( ( [C.] Or A /\ e e. A ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) )
47 sseq1 
 |-  ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
48 sseq2 
 |-  ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
49 47 48 orbi12d 
 |-  ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
50 49 ralbidv 
 |-  ( x = ( e \ C ) -> ( A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) <-> A. f e. ran ( g e. A |-> ( g \ C ) ) ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
51 46 50 syl5ibrcom 
 |-  ( ( [C.] Or A /\ e e. A ) -> ( x = ( e \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
52 51 rexlimdva 
 |-  ( [C.] Or A -> ( E. e e. A x = ( e \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
53 33 52 biimtrid 
 |-  ( [C.] Or A -> ( E. g e. A x = ( g \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
54 30 53 biimtrid 
 |-  ( [C.] Or A -> ( x e. ran ( g e. A |-> ( g \ C ) ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
55 54 ralrimiv 
 |-  ( [C.] Or A -> A. x e. ran ( g e. A |-> ( g \ C ) ) A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) )
56 sorpss 
 |-  ( [C.] Or ran ( g e. A |-> ( g \ C ) ) <-> A. x e. ran ( g e. A |-> ( g \ C ) ) A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) )
57 55 56 sylibr 
 |-  ( [C.] Or A -> [C.] Or ran ( g e. A |-> ( g \ C ) ) )
58 28 57 syl 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> [C.] Or ran ( g e. A |-> ( g \ C ) ) )
59 fin2i 
 |-  ( ( ( ( B \ C ) e. Fin2 /\ ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) ) /\ ( ran ( g e. A |-> ( g \ C ) ) =/= (/) /\ [C.] Or ran ( g e. A |-> ( g \ C ) ) ) ) -> U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
60 1 15 27 58 59 syl22anc 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
61 simpll3 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> -. U. A e. A )
62 difeq1 
 |-  ( g = f -> ( g \ C ) = ( f \ C ) )
63 62 cbvmptv 
 |-  ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
64 63 elrnmpt 
 |-  ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) )
65 64 ibi 
 |-  ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
66 eqid 
 |-  ( h \ C ) = ( h \ C )
67 difeq1 
 |-  ( g = h -> ( g \ C ) = ( h \ C ) )
68 67 rspceeqv 
 |-  ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
69 66 68 mpan2 
 |-  ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
70 69 adantl 
 |-  ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> E. g e. A ( h \ C ) = ( g \ C ) )
71 vex 
 |-  h e. _V
72 difexg 
 |-  ( h e. _V -> ( h \ C ) e. _V )
73 9 elrnmpt 
 |-  ( ( h \ C ) e. _V -> ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( h \ C ) = ( g \ C ) ) )
74 71 72 73 mp2b 
 |-  ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( h \ C ) = ( g \ C ) )
75 70 74 sylibr 
 |-  ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
76 elssuni 
 |-  ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) -> ( h \ C ) C_ U. ran ( g e. A |-> ( g \ C ) ) )
77 75 76 syl 
 |-  ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ U. ran ( g e. A |-> ( g \ C ) ) )
78 simplr 
 |-  ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
79 77 78 sseqtrd 
 |-  ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
80 79 adantll 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
81 unss2 
 |-  ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
82 uncom 
 |-  ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
83 undif1 
 |-  ( ( h \ C ) u. C ) = ( h u. C )
84 82 83 eqtri 
 |-  ( C u. ( h \ C ) ) = ( h u. C )
85 84 a1i 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( C u. ( h \ C ) ) = ( h u. C ) )
86 61 ad2antrr 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> -. U. A e. A )
87 16 ad2antrr 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> C e. A )
88 simplrr 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
89 eqeq1 
 |-  ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
90 simpllr 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
91 ssdif0 
 |-  ( f C_ C <-> ( f \ C ) = (/) )
92 91 biimpi 
 |-  ( f C_ C -> ( f \ C ) = (/) )
93 92 ad2antlr 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( f \ C ) = (/) )
94 90 93 eqtrd 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = (/) )
95 uni0c 
 |-  ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
96 94 95 sylib 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
97 eqid 
 |-  ( x \ C ) = ( x \ C )
98 difeq1 
 |-  ( g = x -> ( g \ C ) = ( x \ C ) )
99 98 rspceeqv 
 |-  ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
100 97 99 mpan2 
 |-  ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
101 vex 
 |-  x e. _V
102 difexg 
 |-  ( x e. _V -> ( x \ C ) e. _V )
103 9 elrnmpt 
 |-  ( ( x \ C ) e. _V -> ( ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( x \ C ) = ( g \ C ) ) )
104 101 102 103 mp2b 
 |-  ( ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( x \ C ) = ( g \ C ) )
105 100 104 sylibr 
 |-  ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
106 105 adantl 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
107 89 96 106 rspcdva 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
108 ssdif0 
 |-  ( x C_ C <-> ( x \ C ) = (/) )
109 107 108 sylibr 
 |-  ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> x C_ C )
110 109 ralrimiva 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> A. x e. A x C_ C )
111 unissb 
 |-  ( U. A C_ C <-> A. x e. A x C_ C )
112 110 111 sylibr 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
113 elssuni 
 |-  ( C e. A -> C C_ U. A )
114 113 ad2antrr 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
115 112 114 eqssd 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
116 simpll 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
117 115 116 eqeltrd 
 |-  ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
118 117 ex 
 |-  ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) -> ( f C_ C -> U. A e. A ) )
119 87 88 118 syl2anc 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( f C_ C -> U. A e. A ) )
120 86 119 mtod 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> -. f C_ C )
121 28 ad2antrr 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> [C.] Or A )
122 simplrl 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> f e. A )
123 sorpssi 
 |-  ( ( [C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
124 121 122 87 123 syl12anc 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( f C_ C \/ C C_ f ) )
125 orel1 
 |-  ( -. f C_ C -> ( ( f C_ C \/ C C_ f ) -> C C_ f ) )
126 120 124 125 sylc 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> C C_ f )
127 undif 
 |-  ( C C_ f <-> ( C u. ( f \ C ) ) = f )
128 126 127 sylib 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( C u. ( f \ C ) ) = f )
129 85 128 sseq12d 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) <-> ( h u. C ) C_ f ) )
130 ssun1 
 |-  h C_ ( h u. C )
131 sstr 
 |-  ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
132 130 131 mpan 
 |-  ( ( h u. C ) C_ f -> h C_ f )
133 129 132 biimtrdi 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) -> h C_ f ) )
134 81 133 syl5 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( h \ C ) C_ ( f \ C ) -> h C_ f ) )
135 80 134 mpd 
 |-  ( ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> h C_ f )
136 135 ralrimiva 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> A. h e. A h C_ f )
137 unissb 
 |-  ( U. A C_ f <-> A. h e. A h C_ f )
138 136 137 sylibr 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A C_ f )
139 elssuni 
 |-  ( f e. A -> f C_ U. A )
140 139 ad2antrl 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> f C_ U. A )
141 138 140 eqssd 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A = f )
142 simprl 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> f e. A )
143 141 142 eqeltrd 
 |-  ( ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A e. A )
144 143 rexlimdvaa 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> ( E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) -> U. A e. A ) )
145 65 144 syl5 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> U. A e. A ) )
146 61 145 mtod 
 |-  ( ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. Fin2 ) -> -. U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
147 60 146 pm2.65da 
 |-  ( ( ( A C_ ~P B /\ [C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) -> -. ( B \ C ) e. Fin2 )