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

Metamath Proof Explorer

Theorem cdlemk40

Description: TODO: fix comment. (Contributed by NM, 31-Jul-2013)

Ref Expression
Hypotheses cdlemk40.x ⊢ X = ι z ∈ T | φ
cdlemk40.u ⊢ U = g ∈ T ⟼ if F = N g X
Assertion cdlemk40 ⊢ G ∈ T → U ⁡ G = if F = N G ⦋ G / g⦌ X

Proof

Step Hyp Ref Expression
1 cdlemk40.x ⊢ X = ι z ∈ T | φ
2 cdlemk40.u ⊢ U = g ∈ T ⟼ if F = N g X
3 vex ⊢ g ∈ V
4 riotaex ⊢ ι z ∈ T | φ ∈ V
5 1 4 eqeltri ⊢ X ∈ V
6 3 5 ifex ⊢ if F = N g X ∈ V
7 6 csbex ⊢ ⦋ G / g⦌ if F = N g X ∈ V
8 2 fvmpts ⊢ G ∈ T ∧ ⦋ G / g⦌ if F = N g X ∈ V → U ⁡ G = ⦋ G / g⦌ if F = N g X
9 7 8 mpan2 ⊢ G ∈ T → U ⁡ G = ⦋ G / g⦌ if F = N g X
10 csbif ⊢ ⦋ G / g⦌ if F = N g X = if [˙G / g]˙ F = N ⦋ G / g⦌ g ⦋ G / g⦌ X
11 sbcg ⊢ G ∈ T → [˙G / g]˙ F = N ↔ F = N
12 csbvarg ⊢ G ∈ T → ⦋ G / g⦌ g = G
13 11 12 ifbieq1d ⊢ G ∈ T → if [˙G / g]˙ F = N ⦋ G / g⦌ g ⦋ G / g⦌ X = if F = N G ⦋ G / g⦌ X
14 10 13 eqtrid ⊢ G ∈ T → ⦋ G / g⦌ if F = N g X = if F = N G ⦋ G / g⦌ X
15 9 14 eqtrd ⊢ G ∈ T → U ⁡ G = if F = N G ⦋ G / g⦌ X