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

Metamath Proof Explorer

Theorem fin23lem15

Description: Lemma for fin23 . U is a monotone function. (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 fin23lem15 ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A → U ⁡ A ⊆ U ⁡ B

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 ⊢ b = B → U ⁡ b = U ⁡ B
3 2 sseq1d ⊢ b = B → U ⁡ b ⊆ U ⁡ B ↔ U ⁡ B ⊆ U ⁡ B
4 fveq2 ⊢ b = a → U ⁡ b = U ⁡ a
5 4 sseq1d ⊢ b = a → U ⁡ b ⊆ U ⁡ B ↔ U ⁡ a ⊆ U ⁡ B
6 fveq2 ⊢ b = suc ⁡ a → U ⁡ b = U ⁡ suc ⁡ a
7 6 sseq1d ⊢ b = suc ⁡ a → U ⁡ b ⊆ U ⁡ B ↔ U ⁡ suc ⁡ a ⊆ U ⁡ B
8 fveq2 ⊢ b = A → U ⁡ b = U ⁡ A
9 8 sseq1d ⊢ b = A → U ⁡ b ⊆ U ⁡ B ↔ U ⁡ A ⊆ U ⁡ B
10 ssidd ⊢ B ∈ ω → U ⁡ B ⊆ U ⁡ B
11 1 fin23lem13 ⊢ a ∈ ω → U ⁡ suc ⁡ a ⊆ U ⁡ a
12 11 ad2antrr ⊢ a ∈ ω ∧ B ∈ ω ∧ B ⊆ a → U ⁡ suc ⁡ a ⊆ U ⁡ a
13 sstr2 ⊢ U ⁡ suc ⁡ a ⊆ U ⁡ a → U ⁡ a ⊆ U ⁡ B → U ⁡ suc ⁡ a ⊆ U ⁡ B
14 12 13 syl ⊢ a ∈ ω ∧ B ∈ ω ∧ B ⊆ a → U ⁡ a ⊆ U ⁡ B → U ⁡ suc ⁡ a ⊆ U ⁡ B
15 3 5 7 9 10 14 findsg ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A → U ⁡ A ⊆ U ⁡ B