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	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐵 ) )