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 ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
Assertion fin23lem15 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ 𝐵 ) )
3 2 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ 𝐵 ) ↔ ( 𝑈 ‘ 𝐵 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
4 fveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ 𝑎 ) )
5 4 sseq1d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ 𝐵 ) ↔ ( 𝑈 ‘ 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
6 fveq2 ⊢ ( 𝑏 = suc 𝑎 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ suc 𝑎 ) )
7 6 sseq1d ⊢ ( 𝑏 = suc 𝑎 → ( ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ 𝐵 ) ↔ ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
8 fveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ 𝐴 ) )
9 8 sseq1d ⊢ ( 𝑏 = 𝐴 → ( ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ 𝐵 ) ↔ ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
10 ssidd ⊢ ( 𝐵 ∈ ω → ( 𝑈 ‘ 𝐵 ) ⊆ ( 𝑈 ‘ 𝐵 ) )
11 1 fin23lem13 ⊢ ( 𝑎 ∈ ω → ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝑎 ) )
12 11 ad2antrr ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) → ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝑎 ) )
13 sstr2 ⊢ ( ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) → ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
14 12 13 syl ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) → ( 𝑈 ‘ suc 𝑎 ) ⊆ ( 𝑈 ‘ 𝐵 ) ) )
15 3 5 7 9 10 14 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐵 ) )