Metamath Proof Explorer

Theorem fin1a2lem11

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

Ref Expression
Assertion fin1a2lem11 ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b = ∅ → ⋃ c ∈ A | c ≼ b ∈ ∅
10 9 olcd ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → c ∈ A | c ≼ b ≠ ∅
13 fin1a2lem9 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω → c ∈ A | c ≼ b ∈ Fin
14 13 ad4ant123 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → c ∈ A | c ≼ b ∈ Fin
15 simplll ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → [⊂] Or A
16 soss ⊢ c ∈ A | c ≼ b ⊆ A → [⊂] Or A → [⊂] Or c ∈ A | c ≼ b
17 11 15 16 mpsyl ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → [⊂] Or c ∈ A | c ≼ b
18 fin1a2lem10 ⊢ c ∈ A | c ≼ b ≠ ∅ ∧ c ∈ A | c ≼ b ∈ Fin ∧ [⊂] Or c ∈ A | c ≼ b → ⋃ c ∈ A | c ≼ b ∈ c ∈ A | c ≼ b
19 12 14 17 18 syl3anc ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → ⋃ c ∈ A | c ≼ b ∈ c ∈ A | c ≼ b
20 11 19 sselid ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → ⋃ c ∈ A | c ≼ b ∈ A
21 20 orcd ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω ∧ c ∈ A | c ≼ b ≠ ∅ → ⋃ c ∈ A | c ≼ b ∈ A ∨ ⋃ c ∈ A | c ≼ b ∈ ∅
22 10 21 pm2.61dane ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ b ∈ ω → d = ⋃ c ∈ A | c ≼ b → d ∈ A ∨ d ∈ ∅
27 26 rexlimdva ⊢ [⊂] Or A ∧ A ⊆ Fin → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b → d ∈ A ∨ d ∈ ∅
28 simpr ⊢ [⊂] Or A ∧ A ⊆ Fin → A ⊆ Fin
29 28 sselda ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → d ∈ Fin
30 ficardom ⊢ d ∈ Fin → card ⁡ d ∈ ω
31 29 30 syl ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → card ⁡ d ∈ ω
32 breq1 ⊢ c = d → c ≼ card ⁡ d ↔ d ≼ card ⁡ d
33 simpr ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → d ∈ A
34 ficardid ⊢ d ∈ Fin → card ⁡ d ≈ d
35 29 34 syl ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → d ≼ card ⁡ d
39 32 33 38 elrabd ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ≼ card ⁡ d
45 35 adantr ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ≼ d
48 simpllr ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → A ⊆ Fin
49 simprl ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ∈ A
50 48 49 sseldd ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ∈ Fin
51 29 adantr ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → d ∈ Fin
52 simplll ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → [⊂] Or A
53 simplr ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → d ∈ A
54 sorpssi ⊢ [⊂] Or A ∧ b ∈ A ∧ d ∈ A → b ⊆ d ∨ d ⊆ b
55 52 49 53 54 syl12anc ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ≼ d ↔ b ⊆ d
58 47 57 mpbid ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A ∧ b ∈ A ∧ b ≼ card ⁡ d → b ⊆ d
59 58 ex ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → b ∈ A ∧ b ≼ card ⁡ d → b ⊆ d
60 43 59 biimtrid ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → b ∈ c ∈ A | c ≼ card ⁡ d → b ⊆ d
61 60 ralrimiv ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → ∀ b ∈ c ∈ A | c ≼ card ⁡ d b ⊆ d
62 unissb ⊢ ⋃ c ∈ A | c ≼ card ⁡ d ⊆ d ↔ ∀ b ∈ c ∈ A | c ≼ card ⁡ d b ⊆ d
63 61 62 sylibr ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → ⋃ c ∈ A | c ≼ card ⁡ d ⊆ d
64 41 63 eqssd ⊢ [⊂] Or A ∧ 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 ⊢ [⊂] Or A ∧ A ⊆ Fin ∧ d ∈ A → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b
70 69 ex ⊢ [⊂] Or A ∧ A ⊆ Fin → d ∈ A → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b
71 velsn ⊢ d ∈ ∅ ↔ d = ∅
72 peano1 ⊢ ∅ ∈ ω
73 dom0 ⊢ b ≼ ∅ ↔ b = ∅
74 73 bilani ⊢ b ∈ A ∧ b ≼ ∅ → b = ∅
75 74 a1i ⊢ [⊂] Or A ∧ A ⊆ Fin → b ∈ A ∧ b ≼ ∅ → b = ∅
76 breq1 ⊢ c = b → c ≼ ∅ ↔ b ≼ ∅
77 76 elrab ⊢ b ∈ c ∈ A | c ≼ ∅ ↔ b ∈ A ∧ b ≼ ∅
78 velsn ⊢ b ∈ ∅ ↔ b = ∅
79 75 77 78 3imtr4g ⊢ [⊂] Or A ∧ A ⊆ Fin → b ∈ c ∈ A | c ≼ ∅ → b ∈ ∅
80 79 ssrdv ⊢ [⊂] Or A ∧ A ⊆ Fin → c ∈ A | c ≼ ∅ ⊆ ∅
81 uni0b ⊢ ⋃ c ∈ A | c ≼ ∅ = ∅ ↔ c ∈ A | c ≼ ∅ ⊆ ∅
82 80 81 sylibr ⊢ [⊂] Or A ∧ A ⊆ Fin → ⋃ c ∈ A | c ≼ ∅ = ∅
83 82 eqcomd ⊢ [⊂] Or A ∧ A ⊆ Fin → ∅ = ⋃ c ∈ A | c ≼ ∅
84 breq2 ⊢ b = ∅ → c ≼ b ↔ c ≼ ∅
85 84 rabbidv ⊢ b = ∅ → c ∈ A | c ≼ b = c ∈ A | c ≼ ∅
86 85 unieqd ⊢ b = ∅ → ⋃ c ∈ A | c ≼ b = ⋃ c ∈ A | c ≼ ∅
87 86 rspceeqv ⊢ ∅ ∈ ω ∧ ∅ = ⋃ c ∈ A | c ≼ ∅ → ∃ b ∈ ω ∅ = ⋃ c ∈ A | c ≼ b
88 72 83 87 sylancr ⊢ [⊂] Or A ∧ A ⊆ Fin → ∃ b ∈ ω ∅ = ⋃ c ∈ A | c ≼ b
89 eqeq1 ⊢ d = ∅ → d = ⋃ c ∈ A | c ≼ b ↔ ∅ = ⋃ c ∈ A | c ≼ b
90 89 rexbidv ⊢ d = ∅ → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b ↔ ∃ b ∈ ω ∅ = ⋃ c ∈ A | c ≼ b
91 88 90 syl5ibrcom ⊢ [⊂] Or A ∧ A ⊆ Fin → d = ∅ → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b
92 71 91 biimtrid ⊢ [⊂] Or A ∧ A ⊆ Fin → d ∈ ∅ → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b
93 70 92 jaod ⊢ [⊂] Or A ∧ A ⊆ Fin → d ∈ A ∨ d ∈ ∅ → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b
94 27 93 impbid ⊢ [⊂] Or A ∧ A ⊆ Fin → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b ↔ d ∈ A ∨ d ∈ ∅
95 elun ⊢ d ∈ A ∪ ∅ ↔ d ∈ A ∨ d ∈ ∅
96 94 95 bitr4di ⊢ [⊂] Or A ∧ A ⊆ Fin → ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b ↔ d ∈ A ∪ ∅
97 96 eqabcdv ⊢ [⊂] Or A ∧ A ⊆ Fin → d | ∃ b ∈ ω d = ⋃ c ∈ A | c ≼ b = A ∪ ∅
98 2 97 eqtrid ⊢ [⊂] Or A ∧ A ⊆ Fin → ran ⁡ b ∈ ω ⟼ ⋃ c ∈ A | c ≼ b = A ∪ ∅