Theorem fin23lem13

Description: Lemma for fin23 . Each step of U is a decrease. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Hypothesis	fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
Assertion	fin23lem13	⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑈 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2	1	fin23lem12	⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) )
3		sseq1	⊢ ( ( 𝑈 ‘ 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) → ( ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐴 ) ↔ if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ⊆ ( 𝑈 ‘ 𝐴 ) ) )
4		sseq1	⊢ ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) → ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ⊆ ( 𝑈 ‘ 𝐴 ) ↔ if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ⊆ ( 𝑈 ‘ 𝐴 ) ) )
5		ssid	⊢ ( 𝑈 ‘ 𝐴 ) ⊆ ( 𝑈 ‘ 𝐴 )
6		inss2	⊢ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ⊆ ( 𝑈 ‘ 𝐴 )
7	3 4 5 6	keephyp	⊢ if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ⊆ ( 𝑈 ‘ 𝐴 )
8	2 7	eqsstrdi	⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑈 ‘ 𝐴 ) )