Metamath Proof Explorer

Theorem fin1a2lem11

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fin1a2lem11 
|- ( ( [C.] Or A /\ A C_ Fin ) -> ran ( b e. _om |-> U. { c e. A | c ~<_ b } ) = ( A u. { (/) } ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( b e. _om |-> U. { c e. A | c ~<_ b } ) = ( b e. _om |-> U. { c e. A | c ~<_ b } )
2 1 rnmpt 
 |-  ran ( b e. _om |-> U. { c e. A | c ~<_ b } ) = { d | E. b e. _om d = U. { c e. A | c ~<_ b } }
3 unieq 
 |-  ( { c e. A | c ~<_ b } = (/) -> U. { c e. A | c ~<_ b } = U. (/) )
4 uni0 
 |-  U. (/) = (/)
5 3 4 eqtrdi 
 |-  ( { c e. A | c ~<_ b } = (/) -> U. { c e. A | c ~<_ b } = (/) )
6 5 adantl 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } = (/) ) -> U. { c e. A | c ~<_ b } = (/) )
7 0ex 
 |-  (/) e. _V
8 7 elsn2 
 |-  ( U. { c e. A | c ~<_ b } e. { (/) } <-> U. { c e. A | c ~<_ b } = (/) )
9 6 8 sylibr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } = (/) ) -> U. { c e. A | c ~<_ b } e. { (/) } )
10 9 olcd 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } = (/) ) -> ( U. { c e. A | c ~<_ b } e. A \/ U. { c e. A | c ~<_ b } e. { (/) } ) )
11 ssrab2 
 |-  { c e. A | c ~<_ b } C_ A
12 simpr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> { c e. A | c ~<_ b } =/= (/) )
13 fin1a2lem9 
 |-  ( ( [C.] Or A /\ A C_ Fin /\ b e. _om ) -> { c e. A | c ~<_ b } e. Fin )
14 13 ad4ant123 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> { c e. A | c ~<_ b } e. Fin )
15 simplll 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> [C.] Or A )
16 soss 
 |-  ( { c e. A | c ~<_ b } C_ A -> ( [C.] Or A -> [C.] Or { c e. A | c ~<_ b } ) )
17 11 15 16 mpsyl 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> [C.] Or { c e. A | c ~<_ b } )
18 fin1a2lem10 
 |-  ( ( { c e. A | c ~<_ b } =/= (/) /\ { c e. A | c ~<_ b } e. Fin /\ [C.] Or { c e. A | c ~<_ b } ) -> U. { c e. A | c ~<_ b } e. { c e. A | c ~<_ b } )
19 12 14 17 18 syl3anc 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> U. { c e. A | c ~<_ b } e. { c e. A | c ~<_ b } )
20 11 19 sseldi 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> U. { c e. A | c ~<_ b } e. A )
21 20 orcd 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) /\ { c e. A | c ~<_ b } =/= (/) ) -> ( U. { c e. A | c ~<_ b } e. A \/ U. { c e. A | c ~<_ b } e. { (/) } ) )
22 10 21 pm2.61dane 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) -> ( U. { c e. A | c ~<_ b } e. A \/ U. { c e. A | c ~<_ b } e. { (/) } ) )
23 eleq1 
 |-  ( d = U. { c e. A | c ~<_ b } -> ( d e. A <-> U. { c e. A | c ~<_ b } e. A ) )
24 eleq1 
 |-  ( d = U. { c e. A | c ~<_ b } -> ( d e. { (/) } <-> U. { c e. A | c ~<_ b } e. { (/) } ) )
25 23 24 orbi12d 
 |-  ( d = U. { c e. A | c ~<_ b } -> ( ( d e. A \/ d e. { (/) } ) <-> ( U. { c e. A | c ~<_ b } e. A \/ U. { c e. A | c ~<_ b } e. { (/) } ) ) )
26 22 25 syl5ibrcom 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ b e. _om ) -> ( d = U. { c e. A | c ~<_ b } -> ( d e. A \/ d e. { (/) } ) ) )
27 26 rexlimdva 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( E. b e. _om d = U. { c e. A | c ~<_ b } -> ( d e. A \/ d e. { (/) } ) ) )
28 simpr 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> A C_ Fin )
29 28 sselda 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d e. Fin )
30 ficardom 
 |-  ( d e. Fin -> ( card ` d ) e. _om )
31 29 30 syl 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> ( card ` d ) e. _om )
32 breq1 
 |-  ( c = d -> ( c ~<_ ( card ` d ) <-> d ~<_ ( card ` d ) ) )
33 simpr 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d e. A )
34 ficardid 
 |-  ( d e. Fin -> ( card ` d ) ~~ d )
35 29 34 syl 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> ( card ` d ) ~~ d )
36 ensym 
 |-  ( ( card ` d ) ~~ d -> d ~~ ( card ` d ) )
37 endom 
 |-  ( d ~~ ( card ` d ) -> d ~<_ ( card ` d ) )
38 35 36 37 3syl 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d ~<_ ( card ` d ) )
39 32 33 38 elrabd 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d e. { c e. A | c ~<_ ( card ` d ) } )
40 elssuni 
 |-  ( d e. { c e. A | c ~<_ ( card ` d ) } -> d C_ U. { c e. A | c ~<_ ( card ` d ) } )
41 39 40 syl 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d C_ U. { c e. A | c ~<_ ( card ` d ) } )
42 breq1 
 |-  ( c = b -> ( c ~<_ ( card ` d ) <-> b ~<_ ( card ` d ) ) )
43 42 elrab 
 |-  ( b e. { c e. A | c ~<_ ( card ` d ) } <-> ( b e. A /\ b ~<_ ( card ` d ) ) )
44 simprr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> b ~<_ ( card ` d ) )
45 35 adantr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> ( card ` d ) ~~ d )
46 domentr 
 |-  ( ( b ~<_ ( card ` d ) /\ ( card ` d ) ~~ d ) -> b ~<_ d )
47 44 45 46 syl2anc 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> b ~<_ d )
48 simpllr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> A C_ Fin )
49 simprl 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> b e. A )
50 48 49 sseldd 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> b e. Fin )
51 29 adantr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> d e. Fin )
52 simplll 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> [C.] Or A )
53 simplr 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> d e. A )
54 sorpssi 
 |-  ( ( [C.] Or A /\ ( b e. A /\ d e. A ) ) -> ( b C_ d \/ d C_ b ) )
55 52 49 53 54 syl12anc 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> ( b C_ d \/ d C_ b ) )
56 fincssdom 
 |-  ( ( b e. Fin /\ d e. Fin /\ ( b C_ d \/ d C_ b ) ) -> ( b ~<_ d <-> b C_ d ) )
57 50 51 55 56 syl3anc 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> ( b ~<_ d <-> b C_ d ) )
58 47 57 mpbid 
 |-  ( ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) /\ ( b e. A /\ b ~<_ ( card ` d ) ) ) -> b C_ d )
59 58 ex 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> ( ( b e. A /\ b ~<_ ( card ` d ) ) -> b C_ d ) )
60 43 59 syl5bi 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> ( b e. { c e. A | c ~<_ ( card ` d ) } -> b C_ d ) )
61 60 ralrimiv 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> A. b e. { c e. A | c ~<_ ( card ` d ) } b C_ d )
62 unissb 
 |-  ( U. { c e. A | c ~<_ ( card ` d ) } C_ d <-> A. b e. { c e. A | c ~<_ ( card ` d ) } b C_ d )
63 61 62 sylibr 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> U. { c e. A | c ~<_ ( card ` d ) } C_ d )
64 41 63 eqssd 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> d = U. { c e. A | c ~<_ ( card ` d ) } )
65 breq2 
 |-  ( b = ( card ` d ) -> ( c ~<_ b <-> c ~<_ ( card ` d ) ) )
66 65 rabbidv 
 |-  ( b = ( card ` d ) -> { c e. A | c ~<_ b } = { c e. A | c ~<_ ( card ` d ) } )
67 66 unieqd 
 |-  ( b = ( card ` d ) -> U. { c e. A | c ~<_ b } = U. { c e. A | c ~<_ ( card ` d ) } )
68 67 rspceeqv 
 |-  ( ( ( card ` d ) e. _om /\ d = U. { c e. A | c ~<_ ( card ` d ) } ) -> E. b e. _om d = U. { c e. A | c ~<_ b } )
69 31 64 68 syl2anc 
 |-  ( ( ( [C.] Or A /\ A C_ Fin ) /\ d e. A ) -> E. b e. _om d = U. { c e. A | c ~<_ b } )
70 69 ex 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( d e. A -> E. b e. _om d = U. { c e. A | c ~<_ b } ) )
71 velsn 
 |-  ( d e. { (/) } <-> d = (/) )
72 peano1 
 |-  (/) e. _om
73 dom0 
 |-  ( b ~<_ (/) <-> b = (/) )
74 73 biimpi 
 |-  ( b ~<_ (/) -> b = (/) )
75 74 adantl 
 |-  ( ( b e. A /\ b ~<_ (/) ) -> b = (/) )
76 75 a1i 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( ( b e. A /\ b ~<_ (/) ) -> b = (/) ) )
77 breq1 
 |-  ( c = b -> ( c ~<_ (/) <-> b ~<_ (/) ) )
78 77 elrab 
 |-  ( b e. { c e. A | c ~<_ (/) } <-> ( b e. A /\ b ~<_ (/) ) )
79 velsn 
 |-  ( b e. { (/) } <-> b = (/) )
80 76 78 79 3imtr4g 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( b e. { c e. A | c ~<_ (/) } -> b e. { (/) } ) )
81 80 ssrdv 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> { c e. A | c ~<_ (/) } C_ { (/) } )
82 uni0b 
 |-  ( U. { c e. A | c ~<_ (/) } = (/) <-> { c e. A | c ~<_ (/) } C_ { (/) } )
83 81 82 sylibr 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> U. { c e. A | c ~<_ (/) } = (/) )
84 83 eqcomd 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> (/) = U. { c e. A | c ~<_ (/) } )
85 breq2 
 |-  ( b = (/) -> ( c ~<_ b <-> c ~<_ (/) ) )
86 85 rabbidv 
 |-  ( b = (/) -> { c e. A | c ~<_ b } = { c e. A | c ~<_ (/) } )
87 86 unieqd 
 |-  ( b = (/) -> U. { c e. A | c ~<_ b } = U. { c e. A | c ~<_ (/) } )
88 87 rspceeqv 
 |-  ( ( (/) e. _om /\ (/) = U. { c e. A | c ~<_ (/) } ) -> E. b e. _om (/) = U. { c e. A | c ~<_ b } )
89 72 84 88 sylancr 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> E. b e. _om (/) = U. { c e. A | c ~<_ b } )
90 eqeq1 
 |-  ( d = (/) -> ( d = U. { c e. A | c ~<_ b } <-> (/) = U. { c e. A | c ~<_ b } ) )
91 90 rexbidv 
 |-  ( d = (/) -> ( E. b e. _om d = U. { c e. A | c ~<_ b } <-> E. b e. _om (/) = U. { c e. A | c ~<_ b } ) )
92 89 91 syl5ibrcom 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( d = (/) -> E. b e. _om d = U. { c e. A | c ~<_ b } ) )
93 71 92 syl5bi 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( d e. { (/) } -> E. b e. _om d = U. { c e. A | c ~<_ b } ) )
94 70 93 jaod 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( ( d e. A \/ d e. { (/) } ) -> E. b e. _om d = U. { c e. A | c ~<_ b } ) )
95 27 94 impbid 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( E. b e. _om d = U. { c e. A | c ~<_ b } <-> ( d e. A \/ d e. { (/) } ) ) )
96 elun 
 |-  ( d e. ( A u. { (/) } ) <-> ( d e. A \/ d e. { (/) } ) )
97 95 96 bitr4di 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ( E. b e. _om d = U. { c e. A | c ~<_ b } <-> d e. ( A u. { (/) } ) ) )
98 97 abbi1dv 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> { d | E. b e. _om d = U. { c e. A | c ~<_ b } } = ( A u. { (/) } ) )
99 2 98 syl5eq 
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ran ( b e. _om |-> U. { c e. A | c ~<_ b } ) = ( A u. { (/) } ) )