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∈ns⁡suc⁡k∈F⁡s⁡k
axdc3lem3.3 ⊢B∈V
Assertion axdc3lem3 ⊢B∈S↔∃m∈ωB:suc⁡m⟶A∧B⁡∅=C∧∀k∈mB⁡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∈ns⁡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∈ns⁡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∈ns⁡suc⁡k∈F⁡s⁡k↔∀k∈nB⁡suc⁡k∈F⁡B⁡k
13 5 7 12 3anbi123d ⊢s=B→s:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k↔B:suc⁡n⟶A∧B⁡∅=C∧∀k∈nB⁡suc⁡k∈F⁡B⁡k
14 13 rexbidv ⊢s=B→∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k↔∃n∈ωB:suc⁡n⟶A∧B⁡∅=C∧∀k∈nB⁡suc⁡k∈F⁡B⁡k
15 3 14 elab ⊢B∈s|∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k↔∃n∈ωB:suc⁡n⟶A∧B⁡∅=C∧∀k∈nB⁡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∈nB⁡suc⁡k∈F⁡B⁡k↔∀k∈mB⁡suc⁡k∈F⁡B⁡k
19 17 18 3anbi13d ⊢n=m→B:suc⁡n⟶A∧B⁡∅=C∧∀k∈nB⁡suc⁡k∈F⁡B⁡k↔B:suc⁡m⟶A∧B⁡∅=C∧∀k∈mB⁡suc⁡k∈F⁡B⁡k
20 19 cbvrexvw ⊢∃n∈ωB:suc⁡n⟶A∧B⁡∅=C∧∀k∈nB⁡suc⁡k∈F⁡B⁡k↔∃m∈ωB:suc⁡m⟶A∧B⁡∅=C∧∀k∈mB⁡suc⁡k∈F⁡B⁡k
21 4 15 20 3bitri ⊢B∈S↔∃m∈ωB:suc⁡m⟶A∧B⁡∅=C∧∀k∈mB⁡suc⁡k∈F⁡B⁡k