Metamath Proof Explorer

Theorem fin23lem14

Description: Lemma for fin23 . U will never evolve to an empty set if it did not start with one. (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 fin23lem14 ⊢ A ∈ ω ∧ ⋃ ran ⁡ t ≠ ∅ → U ⁡ A ≠ ∅

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
2 fveq2 ⊢ a = ∅ → U ⁡ a = U ⁡ ∅
3 2 neeq1d ⊢ a = ∅ → U ⁡ a ≠ ∅ ↔ U ⁡ ∅ ≠ ∅
4 3 imbi2d ⊢ a = ∅ → ⋃ ran ⁡ t ≠ ∅ → U ⁡ a ≠ ∅ ↔ ⋃ ran ⁡ t ≠ ∅ → U ⁡ ∅ ≠ ∅
5 fveq2 ⊢ a = b → U ⁡ a = U ⁡ b
6 5 neeq1d ⊢ a = b → U ⁡ a ≠ ∅ ↔ U ⁡ b ≠ ∅
7 6 imbi2d ⊢ a = b → ⋃ ran ⁡ t ≠ ∅ → U ⁡ a ≠ ∅ ↔ ⋃ ran ⁡ t ≠ ∅ → U ⁡ b ≠ ∅
8 fveq2 ⊢ a = suc ⁡ b → U ⁡ a = U ⁡ suc ⁡ b
9 8 neeq1d ⊢ a = suc ⁡ b → U ⁡ a ≠ ∅ ↔ U ⁡ suc ⁡ b ≠ ∅
10 9 imbi2d ⊢ a = suc ⁡ b → ⋃ ran ⁡ t ≠ ∅ → U ⁡ a ≠ ∅ ↔ ⋃ ran ⁡ t ≠ ∅ → U ⁡ suc ⁡ b ≠ ∅
11 fveq2 ⊢ a = A → U ⁡ a = U ⁡ A
12 11 neeq1d ⊢ a = A → U ⁡ a ≠ ∅ ↔ U ⁡ A ≠ ∅
13 12 imbi2d ⊢ a = A → ⋃ ran ⁡ t ≠ ∅ → U ⁡ a ≠ ∅ ↔ ⋃ ran ⁡ t ≠ ∅ → U ⁡ A ≠ ∅
14 vex ⊢ t ∈ V
15 14 rnex ⊢ ran ⁡ t ∈ V
16 15 uniex ⊢ ⋃ ran ⁡ t ∈ V
17 1 seqom0g ⊢ ⋃ ran ⁡ t ∈ V → U ⁡ ∅ = ⋃ ran ⁡ t
18 16 17 mp1i ⊢ ⋃ ran ⁡ t ≠ ∅ → U ⁡ ∅ = ⋃ ran ⁡ t
19 id ⊢ ⋃ ran ⁡ t ≠ ∅ → ⋃ ran ⁡ t ≠ ∅
20 18 19 eqnetrd ⊢ ⋃ ran ⁡ t ≠ ∅ → U ⁡ ∅ ≠ ∅
21 1 fin23lem12 ⊢ b ∈ ω → U ⁡ suc ⁡ b = if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b
22 21 adantr ⊢ b ∈ ω ∧ U ⁡ b ≠ ∅ → U ⁡ suc ⁡ b = if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b
23 iftrue ⊢ t ⁡ b ∩ U ⁡ b = ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b = U ⁡ b
24 23 adantr ⊢ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b = U ⁡ b
25 simprr ⊢ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → U ⁡ b ≠ ∅
26 24 25 eqnetrd ⊢ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b ≠ ∅
27 iffalse ⊢ ¬ t ⁡ b ∩ U ⁡ b = ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b = t ⁡ b ∩ U ⁡ b
28 27 adantr ⊢ ¬ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b = t ⁡ b ∩ U ⁡ b
29 neqne ⊢ ¬ t ⁡ b ∩ U ⁡ b = ∅ → t ⁡ b ∩ U ⁡ b ≠ ∅
30 29 adantr ⊢ ¬ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → t ⁡ b ∩ U ⁡ b ≠ ∅
31 28 30 eqnetrd ⊢ ¬ t ⁡ b ∩ U ⁡ b = ∅ ∧ b ∈ ω ∧ U ⁡ b ≠ ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b ≠ ∅
32 26 31 pm2.61ian ⊢ b ∈ ω ∧ U ⁡ b ≠ ∅ → if t ⁡ b ∩ U ⁡ b = ∅ U ⁡ b t ⁡ b ∩ U ⁡ b ≠ ∅
33 22 32 eqnetrd ⊢ b ∈ ω ∧ U ⁡ b ≠ ∅ → U ⁡ suc ⁡ b ≠ ∅
34 33 ex ⊢ b ∈ ω → U ⁡ b ≠ ∅ → U ⁡ suc ⁡ b ≠ ∅
35 34 imim2d ⊢ b ∈ ω → ⋃ ran ⁡ t ≠ ∅ → U ⁡ b ≠ ∅ → ⋃ ran ⁡ t ≠ ∅ → U ⁡ suc ⁡ b ≠ ∅
36 4 7 10 13 20 35 finds ⊢ A ∈ ω → ⋃ ran ⁡ t ≠ ∅ → U ⁡ A ≠ ∅
37 36 imp ⊢ A ∈ ω ∧ ⋃ ran ⁡ t ≠ ∅ → U ⁡ A ≠ ∅