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

Metamath Proof Explorer

Theorem fin23lem36

Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
Assertion fin23lem36 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
3 fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
4 fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
5 fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
6 fveq2 ⊢ ( 𝑎 = 𝐵 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐵 ) )
7 6 rneqd ⊢ ( 𝑎 = 𝐵 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝐵 ) )
8 7 unieqd ⊢ ( 𝑎 = 𝐵 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝐵 ) )
9 8 sseq1d ⊢ ( 𝑎 = 𝐵 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
10 9 imbi2d ⊢ ( 𝑎 = 𝐵 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
11 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝑏 ) )
12 11 rneqd ⊢ ( 𝑎 = 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝑏 ) )
13 12 unieqd ⊢ ( 𝑎 = 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
14 13 sseq1d ⊢ ( 𝑎 = 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
15 14 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
16 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ suc 𝑏 ) )
17 16 rneqd ⊢ ( 𝑎 = suc 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ suc 𝑏 ) )
18 17 unieqd ⊢ ( 𝑎 = suc 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ suc 𝑏 ) )
19 18 sseq1d ⊢ ( 𝑎 = suc 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
20 19 imbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
21 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐴 ) )
22 21 rneqd ⊢ ( 𝑎 = 𝐴 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝐴 ) )
23 22 unieqd ⊢ ( 𝑎 = 𝐴 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝐴 ) )
24 23 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ↔ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
25 24 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ↔ ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
26 ssid ⊢ ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 )
27 26 2a1i ⊢ ( 𝐵 ∈ ω → ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐵 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
28 simprr ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → 𝜑 )
29 simpll ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → 𝑏 ∈ ω )
30 1 2 3 4 5 fin23lem35 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ω ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) )
31 28 29 30 syl2anc ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) )
32 31 pssssd ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) )
33 sstr2 ⊢ ( ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
34 32 33 syl ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝑏 ∧ 𝜑 ) ) → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
35 34 expr ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( 𝜑 → ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
36 35 a2d ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) → ( 𝜑 → ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) ) )
37 10 15 20 25 27 36 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝜑 → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) ) )
38 37 impr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ ∪ ran ( 𝑌 ‘ 𝐵 ) )