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

Metamath Proof Explorer

Theorem cdlemk41

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013)

Ref Expression
Hypothesis cdlemk41.y ⊢ 𝑌 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) )
Assertion cdlemk41 ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ 𝑌 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk41.y ⊢ 𝑌 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) )
2 nfcvd ⊢ ( 𝐺 ∈ 𝑇 → Ⅎ 𝑔 ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) ) )
3 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝑅 ‘ 𝑔 ) = ( 𝑅 ‘ 𝐺 ) )
4 3 oveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) = ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
5 coeq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∘ ◡ 𝑏 ) = ( 𝐺 ∘ ◡ 𝑏 ) )
6 5 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) = ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) )
7 6 oveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) = ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) )
8 4 7 oveq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) ) )
9 1 8 eqtrid ⊢ ( 𝑔 = 𝐺 → 𝑌 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) ) )
10 2 9 csbiegf ⊢ ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ 𝑌 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝑏 ) ) ) ) )