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 sselid
 |-  ( ( ( ( [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 eqtrid
 |-  ( ( [C.] Or A /\ A C_ Fin ) -> ran ( b e. _om |-> U. { c e. A | c ~<_ b } ) = ( A u. { (/) } ) )