Metamath Proof Explorer

Theorem axdc3lem3

Description: Simple substitution lemma for axdc3 . (Contributed by Mario Carneiro, 27-Jan-2013)

Ref Expression
Hypotheses axdc3lem3.1 ⊢ A ∈ V
axdc3lem3.2 ⊢ S = s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
axdc3lem3.3 ⊢ B ∈ V
Assertion axdc3lem3 ⊢ B ∈ S ↔ ∃ m ∈ ω B : suc ⁡ m ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ m B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k

Proof

Step Hyp Ref Expression
1 axdc3lem3.1 ⊢ A ∈ V
2 axdc3lem3.2 ⊢ S = s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
3 axdc3lem3.3 ⊢ B ∈ V
4 2 eleq2i ⊢ B ∈ S ↔ B ∈ s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k
5 feq1 ⊢ s = B → s : suc ⁡ n ⟶ A ↔ B : suc ⁡ n ⟶ A
6 fveq1 ⊢ s = B → s ⁡ ∅ = B ⁡ ∅
7 6 eqeq1d ⊢ s = B → s ⁡ ∅ = C ↔ B ⁡ ∅ = C
8 fveq1 ⊢ s = B → s ⁡ suc ⁡ k = B ⁡ suc ⁡ k
9 fveq1 ⊢ s = B → s ⁡ k = B ⁡ k
10 9 fveq2d ⊢ s = B → F ⁡ s ⁡ k = F ⁡ B ⁡ k
11 8 10 eleq12d ⊢ s = B → s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ↔ B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
12 11 ralbidv ⊢ s = B → ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ↔ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
13 5 7 12 3anbi123d ⊢ s = B → s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ↔ B : suc ⁡ n ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
14 13 rexbidv ⊢ s = B → ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ↔ ∃ n ∈ ω B : suc ⁡ n ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
15 3 14 elab ⊢ B ∈ s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ↔ ∃ n ∈ ω B : suc ⁡ n ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
16 suceq ⊢ n = m → suc ⁡ n = suc ⁡ m
17 16 feq2d ⊢ n = m → B : suc ⁡ n ⟶ A ↔ B : suc ⁡ m ⟶ A
18 raleq ⊢ n = m → ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k ↔ ∀ k ∈ m B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
19 17 18 3anbi13d ⊢ n = m → B : suc ⁡ n ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k ↔ B : suc ⁡ m ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ m B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
20 19 cbvrexvw ⊢ ∃ n ∈ ω B : suc ⁡ n ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ n B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k ↔ ∃ m ∈ ω B : suc ⁡ m ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ m B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k
21 4 15 20 3bitri ⊢ B ∈ S ↔ ∃ m ∈ ω B : suc ⁡ m ⟶ A ∧ B ⁡ ∅ = C ∧ ∀ k ∈ m B ⁡ suc ⁡ k ∈ F ⁡ B ⁡ k