Metamath Proof Explorer

Theorem fin1a2lem11

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

Ref Expression
Assertion fin1a2lem11 ⊢[⊂]OrA∧A⊆Fin→ran⁡b∈ω⟼⋃c∈A|c≼b=A∪∅

Proof

Step Hyp Ref Expression
1 eqid ⊢b∈ω⟼⋃c∈A|c≼b=b∈ω⟼⋃c∈A|c≼b
2 1 rnmpt ⊢ran⁡b∈ω⟼⋃c∈A|c≼b=d|∃b∈ωd=⋃c∈A|c≼b
3 unieq ⊢c∈A|c≼b=∅→⋃c∈A|c≼b=⋃∅
4 uni0 ⊢⋃∅=∅
5 3 4 eqtrdi ⊢c∈A|c≼b=∅→⋃c∈A|c≼b=∅
6 5 adantl ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b=∅→⋃c∈A|c≼b=∅
7 0ex ⊢∅∈V
8 7 elsn2 ⊢⋃c∈A|c≼b∈∅↔⋃c∈A|c≼b=∅
9 6 8 sylibr ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b=∅→⋃c∈A|c≼b∈∅
10 9 olcd ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b=∅→⋃c∈A|c≼b∈A∨⋃c∈A|c≼b∈∅
11 ssrab2 ⊢c∈A|c≼b⊆A
12 simpr ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→c∈A|c≼b≠∅
13 fin1a2lem9 ⊢[⊂]OrA∧A⊆Fin∧b∈ω→c∈A|c≼b∈Fin
14 13 ad4ant123 ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→c∈A|c≼b∈Fin
15 simplll ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→[⊂]OrA
16 soss ⊢c∈A|c≼b⊆A→[⊂]OrA→[⊂]Orc∈A|c≼b
17 11 15 16 mpsyl ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→[⊂]Orc∈A|c≼b
18 fin1a2lem10 ⊢c∈A|c≼b≠∅∧c∈A|c≼b∈Fin∧[⊂]Orc∈A|c≼b→⋃c∈A|c≼b∈c∈A|c≼b
19 12 14 17 18 syl3anc ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→⋃c∈A|c≼b∈c∈A|c≼b
20 11 19 sselid ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→⋃c∈A|c≼b∈A
21 20 orcd ⊢[⊂]OrA∧A⊆Fin∧b∈ω∧c∈A|c≼b≠∅→⋃c∈A|c≼b∈A∨⋃c∈A|c≼b∈∅
22 10 21 pm2.61dane ⊢[⊂]OrA∧A⊆Fin∧b∈ω→⋃c∈A|c≼b∈A∨⋃c∈A|c≼b∈∅
23 eleq1 ⊢d=⋃c∈A|c≼b→d∈A↔⋃c∈A|c≼b∈A
24 eleq1 ⊢d=⋃c∈A|c≼b→d∈∅↔⋃c∈A|c≼b∈∅
25 23 24 orbi12d ⊢d=⋃c∈A|c≼b→d∈A∨d∈∅↔⋃c∈A|c≼b∈A∨⋃c∈A|c≼b∈∅
26 22 25 syl5ibrcom ⊢[⊂]OrA∧A⊆Fin∧b∈ω→d=⋃c∈A|c≼b→d∈A∨d∈∅
27 26 rexlimdva ⊢[⊂]OrA∧A⊆Fin→∃b∈ωd=⋃c∈A|c≼b→d∈A∨d∈∅
28 simpr ⊢[⊂]OrA∧A⊆Fin→A⊆Fin
29 28 sselda ⊢[⊂]OrA∧A⊆Fin∧d∈A→d∈Fin
30 ficardom ⊢d∈Fin→card⁡d∈ω
31 29 30 syl ⊢[⊂]OrA∧A⊆Fin∧d∈A→card⁡d∈ω
32 breq1 ⊢c=d→c≼card⁡d↔d≼card⁡d
33 simpr ⊢[⊂]OrA∧A⊆Fin∧d∈A→d∈A
34 ficardid ⊢d∈Fin→card⁡d≈d
35 29 34 syl ⊢[⊂]OrA∧A⊆Fin∧d∈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 ⊢[⊂]OrA∧A⊆Fin∧d∈A→d≼card⁡d
39 32 33 38 elrabd ⊢[⊂]OrA∧A⊆Fin∧d∈A→d∈c∈A|c≼card⁡d
40 elssuni ⊢d∈c∈A|c≼card⁡d→d⊆⋃c∈A|c≼card⁡d
41 39 40 syl ⊢[⊂]OrA∧A⊆Fin∧d∈A→d⊆⋃c∈A|c≼card⁡d
42 breq1 ⊢c=b→c≼card⁡d↔b≼card⁡d
43 42 elrab ⊢b∈c∈A|c≼card⁡d↔b∈A∧b≼card⁡d
44 simprr ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b≼card⁡d
45 35 adantr ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→card⁡d≈d
46 domentr ⊢b≼card⁡d∧card⁡d≈d→b≼d
47 44 45 46 syl2anc ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b≼d
48 simpllr ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→A⊆Fin
49 simprl ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b∈A
50 48 49 sseldd ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b∈Fin
51 29 adantr ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→d∈Fin
52 simplll ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→[⊂]OrA
53 simplr ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→d∈A
54 sorpssi ⊢[⊂]OrA∧b∈A∧d∈A→b⊆d∨d⊆b
55 52 49 53 54 syl12anc ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b⊆d∨d⊆b
56 fincssdom ⊢b∈Fin∧d∈Fin∧b⊆d∨d⊆b→b≼d↔b⊆d
57 50 51 55 56 syl3anc ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b≼d↔b⊆d
58 47 57 mpbid ⊢[⊂]OrA∧A⊆Fin∧d∈A∧b∈A∧b≼card⁡d→b⊆d
59 58 ex ⊢[⊂]OrA∧A⊆Fin∧d∈A→b∈A∧b≼card⁡d→b⊆d
60 43 59 biimtrid ⊢[⊂]OrA∧A⊆Fin∧d∈A→b∈c∈A|c≼card⁡d→b⊆d
61 60 ralrimiv ⊢[⊂]OrA∧A⊆Fin∧d∈A→∀b∈c∈A|c≼card⁡db⊆d
62 unissb ⊢⋃c∈A|c≼card⁡d⊆d↔∀b∈c∈A|c≼card⁡db⊆d
63 61 62 sylibr ⊢[⊂]OrA∧A⊆Fin∧d∈A→⋃c∈A|c≼card⁡d⊆d
64 41 63 eqssd ⊢[⊂]OrA∧A⊆Fin∧d∈A→d=⋃c∈A|c≼card⁡d
65 breq2 ⊢b=card⁡d→c≼b↔c≼card⁡d
66 65 rabbidv ⊢b=card⁡d→c∈A|c≼b=c∈A|c≼card⁡d
67 66 unieqd ⊢b=card⁡d→⋃c∈A|c≼b=⋃c∈A|c≼card⁡d
68 67 rspceeqv ⊢card⁡d∈ω∧d=⋃c∈A|c≼card⁡d→∃b∈ωd=⋃c∈A|c≼b
69 31 64 68 syl2anc ⊢[⊂]OrA∧A⊆Fin∧d∈A→∃b∈ωd=⋃c∈A|c≼b
70 69 ex ⊢[⊂]OrA∧A⊆Fin→d∈A→∃b∈ωd=⋃c∈A|c≼b
71 velsn ⊢d∈∅↔d=∅
72 peano1 ⊢∅∈ω
73 dom0 ⊢b≼∅↔b=∅
74 73 biimpi ⊢b≼∅→b=∅
75 74 adantl ⊢b∈A∧b≼∅→b=∅
76 75 a1i ⊢[⊂]OrA∧A⊆Fin→b∈A∧b≼∅→b=∅
77 breq1 ⊢c=b→c≼∅↔b≼∅
78 77 elrab ⊢b∈c∈A|c≼∅↔b∈A∧b≼∅
79 velsn ⊢b∈∅↔b=∅
80 76 78 79 3imtr4g ⊢[⊂]OrA∧A⊆Fin→b∈c∈A|c≼∅→b∈∅
81 80 ssrdv ⊢[⊂]OrA∧A⊆Fin→c∈A|c≼∅⊆∅
82 uni0b ⊢⋃c∈A|c≼∅=∅↔c∈A|c≼∅⊆∅
83 81 82 sylibr ⊢[⊂]OrA∧A⊆Fin→⋃c∈A|c≼∅=∅
84 83 eqcomd ⊢[⊂]OrA∧A⊆Fin→∅=⋃c∈A|c≼∅
85 breq2 ⊢b=∅→c≼b↔c≼∅
86 85 rabbidv ⊢b=∅→c∈A|c≼b=c∈A|c≼∅
87 86 unieqd ⊢b=∅→⋃c∈A|c≼b=⋃c∈A|c≼∅
88 87 rspceeqv ⊢∅∈ω∧∅=⋃c∈A|c≼∅→∃b∈ω∅=⋃c∈A|c≼b
89 72 84 88 sylancr ⊢[⊂]OrA∧A⊆Fin→∃b∈ω∅=⋃c∈A|c≼b
90 eqeq1 ⊢d=∅→d=⋃c∈A|c≼b↔∅=⋃c∈A|c≼b
91 90 rexbidv ⊢d=∅→∃b∈ωd=⋃c∈A|c≼b↔∃b∈ω∅=⋃c∈A|c≼b
92 89 91 syl5ibrcom ⊢[⊂]OrA∧A⊆Fin→d=∅→∃b∈ωd=⋃c∈A|c≼b
93 71 92 biimtrid ⊢[⊂]OrA∧A⊆Fin→d∈∅→∃b∈ωd=⋃c∈A|c≼b
94 70 93 jaod ⊢[⊂]OrA∧A⊆Fin→d∈A∨d∈∅→∃b∈ωd=⋃c∈A|c≼b
95 27 94 impbid ⊢[⊂]OrA∧A⊆Fin→∃b∈ωd=⋃c∈A|c≼b↔d∈A∨d∈∅
96 elun ⊢d∈A∪∅↔d∈A∨d∈∅
97 95 96 bitr4di ⊢[⊂]OrA∧A⊆Fin→∃b∈ωd=⋃c∈A|c≼b↔d∈A∪∅
98 97 eqabcdv ⊢[⊂]OrA∧A⊆Fin→d|∃b∈ωd=⋃c∈A|c≼b=A∪∅
99 2 98 eqtrid ⊢[⊂]OrA∧A⊆Fin→ran⁡b∈ω⟼⋃c∈A|c≼b=A∪∅