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

Metamath Proof Explorer

Theorem ackbij2lem4

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypotheses ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
Assertion ackbij2lem4 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 ackbij.g ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑦 ∈ 𝒫 dom 𝑥 ↦ ( 𝐹 ‘ ( 𝑥 “ 𝑦 ) ) ) )
3 fveq2 ⊢ ( 𝑎 = 𝐵 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) )
4 3 sseq2d ⊢ ( 𝑎 = 𝐵 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ) )
5 fveq2 ⊢ ( 𝑎 = 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) )
6 5 sseq2d ⊢ ( 𝑎 = 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ) )
7 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
8 7 sseq2d ⊢ ( 𝑎 = suc 𝑏 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
9 fveq2 ⊢ ( 𝑎 = 𝐴 → ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) = ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) )
10 9 sseq2d ⊢ ( 𝑎 = 𝐴 → ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑎 ) ↔ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) ) )
11 ssidd ⊢ ( 𝐵 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) )
12 1 2 ackbij2lem3 ⊢ ( 𝑏 ∈ ω → ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
13 12 ad2antrr ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) )
14 sstr2 ⊢ ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → ( ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
15 13 14 syl5com ⊢ ( ( ( 𝑏 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑏 ) → ( ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝑏 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ suc 𝑏 ) ) )
16 4 6 8 10 11 15 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( rec ( 𝐺 , ∅ ) ‘ 𝐵 ) ⊆ ( rec ( 𝐺 , ∅ ) ‘ 𝐴 ) )