Metamath Proof Explorer

Theorem axdc3lem3

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

Ref Expression
Hypotheses axdc3lem3.1 ⊢ 𝐴 ∈ V
axdc3lem3.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
axdc3lem3.3 ⊢ 𝐵 ∈ V
Assertion axdc3lem3 ( 𝐵 ∈ 𝑆 ↔ ∃ 𝑚 ∈ ω ( 𝐵 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem3.1 ⊢ 𝐴 ∈ V
2 axdc3lem3.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
3 axdc3lem3.3 ⊢ 𝐵 ∈ V
4 2 eleq2i ⊢ ( 𝐵 ∈ 𝑆 ↔ 𝐵 ∈ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } )
5 feq1 ⊢ ( 𝑠 = 𝐵 → ( 𝑠 : suc 𝑛 ⟶ 𝐴 ↔ 𝐵 : suc 𝑛 ⟶ 𝐴 ) )
6 fveq1 ⊢ ( 𝑠 = 𝐵 → ( 𝑠 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) )
7 6 eqeq1d ⊢ ( 𝑠 = 𝐵 → ( ( 𝑠 ‘ ∅ ) = 𝐶 ↔ ( 𝐵 ‘ ∅ ) = 𝐶 ) )
8 fveq1 ⊢ ( 𝑠 = 𝐵 → ( 𝑠 ‘ suc 𝑘 ) = ( 𝐵 ‘ suc 𝑘 ) )
9 fveq1 ⊢ ( 𝑠 = 𝐵 → ( 𝑠 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
10 9 fveq2d ⊢ ( 𝑠 = 𝐵 → ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) )
11 8 10 eleq12d ⊢ ( 𝑠 = 𝐵 → ( ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
12 11 ralbidv ⊢ ( 𝑠 = 𝐵 → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
13 5 7 12 3anbi123d ⊢ ( 𝑠 = 𝐵 → ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ↔ ( 𝐵 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
14 13 rexbidv ⊢ ( 𝑠 = 𝐵 → ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ↔ ∃ 𝑛 ∈ ω ( 𝐵 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
15 3 14 elab ⊢ ( 𝐵 ∈ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ↔ ∃ 𝑛 ∈ ω ( 𝐵 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
16 suceq ⊢ ( 𝑛 = 𝑚 → suc 𝑛 = suc 𝑚 )
17 16 feq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐵 : suc 𝑛 ⟶ 𝐴 ↔ 𝐵 : suc 𝑚 ⟶ 𝐴 ) )
18 raleq ⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝑚 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
19 17 18 3anbi13d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐵 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) ↔ ( 𝐵 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) ) )
20 19 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ω ( 𝐵 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) ↔ ∃ 𝑚 ∈ ω ( 𝐵 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )
21 4 15 20 3bitri ⊢ ( 𝐵 ∈ 𝑆 ↔ ∃ 𝑚 ∈ ω ( 𝐵 : suc 𝑚 ⟶ 𝐴 ∧ ( 𝐵 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑚 ( 𝐵 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐵 ‘ 𝑘 ) ) ) )