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 ( 𝐺 , ∅ ) ‘ 𝐴 ) )