This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin23lem19

Description: Lemma for fin23 . The first set in U to see an input set is either contained in it or disjoint from it. (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 fin23lem19 ⊢ A ∈ ω → U ⁡ suc ⁡ A ⊆ t ⁡ A ∨ U ⁡ suc ⁡ A ∩ t ⁡ 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 1 fin23lem12 ⊢ A ∈ ω → U ⁡ suc ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A
3 eqif ⊢ U ⁡ suc ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A ↔ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = U ⁡ A ∨ ¬ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A
4 2 3 sylib ⊢ A ∈ ω → t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = U ⁡ A ∨ ¬ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A
5 incom ⊢ U ⁡ suc ⁡ A ∩ t ⁡ A = t ⁡ A ∩ U ⁡ suc ⁡ A
6 ineq2 ⊢ U ⁡ suc ⁡ A = U ⁡ A → t ⁡ A ∩ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A
7 6 eqeq1d ⊢ U ⁡ suc ⁡ A = U ⁡ A → t ⁡ A ∩ U ⁡ suc ⁡ A = ∅ ↔ t ⁡ A ∩ U ⁡ A = ∅
8 7 biimparc ⊢ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = U ⁡ A → t ⁡ A ∩ U ⁡ suc ⁡ A = ∅
9 5 8 eqtrid ⊢ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = U ⁡ A → U ⁡ suc ⁡ A ∩ t ⁡ A = ∅
10 inss1 ⊢ t ⁡ A ∩ U ⁡ A ⊆ t ⁡ A
11 sseq1 ⊢ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A → U ⁡ suc ⁡ A ⊆ t ⁡ A ↔ t ⁡ A ∩ U ⁡ A ⊆ t ⁡ A
12 10 11 mpbiri ⊢ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A → U ⁡ suc ⁡ A ⊆ t ⁡ A
13 12 adantl ⊢ ¬ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A → U ⁡ suc ⁡ A ⊆ t ⁡ A
14 9 13 orim12i ⊢ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = U ⁡ A ∨ ¬ t ⁡ A ∩ U ⁡ A = ∅ ∧ U ⁡ suc ⁡ A = t ⁡ A ∩ U ⁡ A → U ⁡ suc ⁡ A ∩ t ⁡ A = ∅ ∨ U ⁡ suc ⁡ A ⊆ t ⁡ A
15 4 14 syl ⊢ A ∈ ω → U ⁡ suc ⁡ A ∩ t ⁡ A = ∅ ∨ U ⁡ suc ⁡ A ⊆ t ⁡ A
16 15 orcomd ⊢ A ∈ ω → U ⁡ suc ⁡ A ⊆ t ⁡ A ∨ U ⁡ suc ⁡ A ∩ t ⁡ A = ∅