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⟼ift⁡i∩u=∅ut⁡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⟼ift⁡i∩u=∅ut⁡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