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

Metamath Proof Explorer

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 𝐴 ) ⊆ ( 𝑈 ‘ 𝐴 ) )