This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnwe2lem1

Description: Lemma for fnwe2 . Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su ⊢ z = F ⁡ x → S = U
fnwe2.t ⊢ T = x y | F ⁡ x R F ⁡ y ∨ F ⁡ x = F ⁡ y ∧ x U y
fnwe2.s ⊢ φ ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
Assertion fnwe2lem1 ⊢ φ ∧ a ∈ A → ⦋ F ⁡ a / z⦌ S We y ∈ A | F ⁡ y = F ⁡ a

Proof

Step Hyp Ref Expression
1 fnwe2.su ⊢ z = F ⁡ x → S = U
2 fnwe2.t ⊢ T = x y | F ⁡ x R F ⁡ y ∨ F ⁡ x = F ⁡ y ∧ x U y
3 fnwe2.s ⊢ φ ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
4 3 ralrimiva ⊢ φ → ∀ x ∈ A U We y ∈ A | F ⁡ y = F ⁡ x
5 fveq2 ⊢ a = x → F ⁡ a = F ⁡ x
6 5 csbeq1d ⊢ a = x → ⦋ F ⁡ a / z⦌ S = ⦋ F ⁡ x / z⦌ S
7 fvex ⊢ F ⁡ x ∈ V
8 7 1 csbie ⊢ ⦋ F ⁡ x / z⦌ S = U
9 6 8 eqtrdi ⊢ a = x → ⦋ F ⁡ a / z⦌ S = U
10 5 eqeq2d ⊢ a = x → F ⁡ y = F ⁡ a ↔ F ⁡ y = F ⁡ x
11 10 rabbidv ⊢ a = x → y ∈ A | F ⁡ y = F ⁡ a = y ∈ A | F ⁡ y = F ⁡ x
12 9 11 weeq12d ⊢ a = x → ⦋ F ⁡ a / z⦌ S We y ∈ A | F ⁡ y = F ⁡ a ↔ U We y ∈ A | F ⁡ y = F ⁡ x
13 12 cbvralvw ⊢ ∀ a ∈ A ⦋ F ⁡ a / z⦌ S We y ∈ A | F ⁡ y = F ⁡ a ↔ ∀ x ∈ A U We y ∈ A | F ⁡ y = F ⁡ x
14 4 13 sylibr ⊢ φ → ∀ a ∈ A ⦋ F ⁡ a / z⦌ S We y ∈ A | F ⁡ y = F ⁡ a
15 14 r19.21bi ⊢ φ ∧ a ∈ A → ⦋ F ⁡ a / z⦌ S We y ∈ A | F ⁡ y = F ⁡ a