Metamath Proof Explorer

Theorem fin23lem16

Description: Lemma for fin23 . U ranges over the original set; in particular ran U is a set, although we do not assume here that U is. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
Assertion fin23lem16 ⊢ ⋃ ran ⁡ U = ⋃ 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 unissb ⊢ ⋃ ran ⁡ U ⊆ ⋃ ran ⁡ t ↔ ∀ a ∈ ran ⁡ U a ⊆ ⋃ ran ⁡ t
3 1 fnseqom ⊢ U Fn ω
4 fvelrnb ⊢ U Fn ω → a ∈ ran ⁡ U ↔ ∃ b ∈ ω U ⁡ b = a
5 3 4 ax-mp ⊢ a ∈ ran ⁡ U ↔ ∃ b ∈ ω U ⁡ b = a
6 peano1 ⊢ ∅ ∈ ω
7 0ss ⊢ ∅ ⊆ b
8 1 fin23lem15 ⊢ b ∈ ω ∧ ∅ ∈ ω ∧ ∅ ⊆ b → U ⁡ b ⊆ U ⁡ ∅
9 7 8 mpan2 ⊢ b ∈ ω ∧ ∅ ∈ ω → U ⁡ b ⊆ U ⁡ ∅
10 6 9 mpan2 ⊢ b ∈ ω → U ⁡ b ⊆ U ⁡ ∅
11 vex ⊢ t ∈ V
12 11 rnex ⊢ ran ⁡ t ∈ V
13 12 uniex ⊢ ⋃ ran ⁡ t ∈ V
14 1 seqom0g ⊢ ⋃ ran ⁡ t ∈ V → U ⁡ ∅ = ⋃ ran ⁡ t
15 13 14 ax-mp ⊢ U ⁡ ∅ = ⋃ ran ⁡ t
16 10 15 sseqtrdi ⊢ b ∈ ω → U ⁡ b ⊆ ⋃ ran ⁡ t
17 sseq1 ⊢ U ⁡ b = a → U ⁡ b ⊆ ⋃ ran ⁡ t ↔ a ⊆ ⋃ ran ⁡ t
18 16 17 syl5ibcom ⊢ b ∈ ω → U ⁡ b = a → a ⊆ ⋃ ran ⁡ t
19 18 rexlimiv ⊢ ∃ b ∈ ω U ⁡ b = a → a ⊆ ⋃ ran ⁡ t
20 5 19 sylbi ⊢ a ∈ ran ⁡ U → a ⊆ ⋃ ran ⁡ t
21 2 20 mprgbir ⊢ ⋃ ran ⁡ U ⊆ ⋃ ran ⁡ t
22 fnfvelrn ⊢ U Fn ω ∧ ∅ ∈ ω → U ⁡ ∅ ∈ ran ⁡ U
23 3 6 22 mp2an ⊢ U ⁡ ∅ ∈ ran ⁡ U
24 15 23 eqeltrri ⊢ ⋃ ran ⁡ t ∈ ran ⁡ U
25 elssuni ⊢ ⋃ ran ⁡ t ∈ ran ⁡ U → ⋃ ran ⁡ t ⊆ ⋃ ran ⁡ U
26 24 25 ax-mp ⊢ ⋃ ran ⁡ t ⊆ ⋃ ran ⁡ U
27 21 26 eqssi ⊢ ⋃ ran ⁡ U = ⋃ ran ⁡ t