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 ⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
cdlemk40.u ⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
Assertion cdlemk40 ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 cdlemk40.x ⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
2 cdlemk40.u ⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
3 vex ⊢ 𝑔 ∈ V
4 riotaex ⊢ ( ℩ 𝑧 ∈ 𝑇 𝜑 ) ∈ V
5 1 4 eqeltri ⊢ 𝑋 ∈ V
6 3 5 ifex ⊢ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V
7 6 csbex ⊢ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V
8 2 fvmpts ⊢ ( ( 𝐺 ∈ 𝑇 ∧ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V ) → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
9 7 8 mpan2 ⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
10 csbif ⊢ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) = if ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 , ⦋ 𝐺 / 𝑔 ⦌ 𝑔 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 )
11 sbcg ⊢ ( 𝐺 ∈ 𝑇 → ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 ↔ 𝐹 = 𝑁 ) )
12 csbvarg ⊢ ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ 𝑔 = 𝐺 )
13 11 12 ifbieq1d ⊢ ( 𝐺 ∈ 𝑇 → if ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 , ⦋ 𝐺 / 𝑔 ⦌ 𝑔 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )
14 10 13 eqtrid ⊢ ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )
15 9 14 eqtrd ⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )