Metamath Proof Explorer

Theorem fin23lem29

Description: Lemma for fin23 . The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
fin23lem17.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
fin23lem.b ⊢ P = v ∈ ω | ⋂ ran ⁡ U ⊆ t ⁡ v
fin23lem.c ⊢ Q = w ∈ ω ⟼ ι x ∈ P | x ∩ P ≈ w
fin23lem.d ⊢ R = w ∈ ω ⟼ ι x ∈ ω ∖ P | x ∩ ω ∖ P ≈ w
fin23lem.e ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
Assertion fin23lem29 ⊢ ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
2 fin23lem17.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
3 fin23lem.b ⊢ P = v ∈ ω | ⋂ ran ⁡ U ⊆ t ⁡ v
4 fin23lem.c ⊢ Q = w ∈ ω ⟼ ι x ∈ P | x ∩ P ≈ w
5 fin23lem.d ⊢ R = w ∈ ω ⟼ ι x ∈ ω ∖ P | x ∩ ω ∖ P ≈ w
6 fin23lem.e ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
7 eqif ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q ↔ P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
8 7 biimpi ⊢ Z = if P ∈ Fin t ∘ R z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
9 rneq ⊢ Z = t ∘ R → ran ⁡ Z = ran ⁡ t ∘ R
10 9 unieqd ⊢ Z = t ∘ R → ⋃ ran ⁡ Z = ⋃ ran ⁡ t ∘ R
11 rncoss ⊢ ran ⁡ t ∘ R ⊆ ran ⁡ t
12 11 unissi ⊢ ⋃ ran ⁡ t ∘ R ⊆ ⋃ ran ⁡ t
13 10 12 eqsstrdi ⊢ Z = t ∘ R → ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t
14 13 adantl ⊢ P ∈ Fin ∧ Z = t ∘ R → ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t
15 rneq ⊢ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → ran ⁡ Z = ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
16 15 unieqd ⊢ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → ⋃ ran ⁡ Z = ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q
17 rncoss ⊢ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q ⊆ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U
18 17 unissi ⊢ ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q ⊆ ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U
19 unissb ⊢ ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⊆ ⋃ ran ⁡ t ↔ ∀ a ∈ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U a ⊆ ⋃ ran ⁡ t
20 abid ⊢ a ∈ a | ∃ z ∈ P a = t ⁡ z ∖ ⋂ ran ⁡ U ↔ ∃ z ∈ P a = t ⁡ z ∖ ⋂ ran ⁡ U
21 fvssunirn ⊢ t ⁡ z ⊆ ⋃ ran ⁡ t
22 21 a1i ⊢ z ∈ P → t ⁡ z ⊆ ⋃ ran ⁡ t
23 22 ssdifssd ⊢ z ∈ P → t ⁡ z ∖ ⋂ ran ⁡ U ⊆ ⋃ ran ⁡ t
24 sseq1 ⊢ a = t ⁡ z ∖ ⋂ ran ⁡ U → a ⊆ ⋃ ran ⁡ t ↔ t ⁡ z ∖ ⋂ ran ⁡ U ⊆ ⋃ ran ⁡ t
25 23 24 syl5ibrcom ⊢ z ∈ P → a = t ⁡ z ∖ ⋂ ran ⁡ U → a ⊆ ⋃ ran ⁡ t
26 25 rexlimiv ⊢ ∃ z ∈ P a = t ⁡ z ∖ ⋂ ran ⁡ U → a ⊆ ⋃ ran ⁡ t
27 20 26 sylbi ⊢ a ∈ a | ∃ z ∈ P a = t ⁡ z ∖ ⋂ ran ⁡ U → a ⊆ ⋃ ran ⁡ t
28 eqid ⊢ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U
29 28 rnmpt ⊢ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U = a | ∃ z ∈ P a = t ⁡ z ∖ ⋂ ran ⁡ U
30 27 29 eleq2s ⊢ a ∈ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U → a ⊆ ⋃ ran ⁡ t
31 19 30 mprgbir ⊢ ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ⊆ ⋃ ran ⁡ t
32 18 31 sstri ⊢ ⋃ ran ⁡ z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q ⊆ ⋃ ran ⁡ t
33 16 32 eqsstrdi ⊢ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t
34 33 adantl ⊢ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t
35 14 34 jaoi ⊢ P ∈ Fin ∧ Z = t ∘ R ∨ ¬ P ∈ Fin ∧ Z = z ∈ P ⟼ t ⁡ z ∖ ⋂ ran ⁡ U ∘ Q → ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t
36 6 8 35 mp2b ⊢ ⋃ ran ⁡ Z ⊆ ⋃ ran ⁡ t