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 ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
ackbij.g ⊢ G = x ∈ V ⟼ y ∈ 𝒫 dom ⁡ x ⟼ F ⁡ x y
Assertion ackbij2lem4 ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ A

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
2 ackbij.g ⊢ G = x ∈ V ⟼ y ∈ 𝒫 dom ⁡ x ⟼ F ⁡ x y
3 fveq2 ⊢ a = B → rec ⁡ G ∅ ⁡ a = rec ⁡ G ∅ ⁡ B
4 3 sseq2d ⊢ a = B → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ a ↔ rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ B
5 fveq2 ⊢ a = b → rec ⁡ G ∅ ⁡ a = rec ⁡ G ∅ ⁡ b
6 5 sseq2d ⊢ a = b → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ a ↔ rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ b
7 fveq2 ⊢ a = suc ⁡ b → rec ⁡ G ∅ ⁡ a = rec ⁡ G ∅ ⁡ suc ⁡ b
8 7 sseq2d ⊢ a = suc ⁡ b → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ a ↔ rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b
9 fveq2 ⊢ a = A → rec ⁡ G ∅ ⁡ a = rec ⁡ G ∅ ⁡ A
10 9 sseq2d ⊢ a = A → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ a ↔ rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ A
11 ssidd ⊢ B ∈ ω → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ B
12 1 2 ackbij2lem3 ⊢ b ∈ ω → rec ⁡ G ∅ ⁡ b ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b
13 12 ad2antrr ⊢ b ∈ ω ∧ B ∈ ω ∧ B ⊆ b → rec ⁡ G ∅ ⁡ b ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b
14 sstr2 ⊢ rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ b → rec ⁡ G ∅ ⁡ b ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b
15 13 14 syl5com ⊢ b ∈ ω ∧ B ∈ ω ∧ B ⊆ b → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ b → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ suc ⁡ b
16 4 6 8 10 11 15 findsg ⊢ A ∈ ω ∧ B ∈ ω ∧ B ⊆ A → rec ⁡ G ∅ ⁡ B ⊆ rec ⁡ G ∅ ⁡ A