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

Metamath Proof Explorer

Theorem fmptcof

Description: Version of fmptco where ph needn't be distinct from x . (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmptcof.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
fmptcof.2 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
fmptcof.3 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
fmptcof.4 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
Assertion fmptcof ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 fmptcof.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
2 fmptcof.2 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
3 fmptcof.3 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
4 fmptcof.4 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
5 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑅
6 5 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵
7 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝑅 = ⦋ 𝑧 / 𝑥 ⦌ 𝑅 )
8 7 eleq1d ⊢ ( 𝑥 = 𝑧 → ( 𝑅 ∈ 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 ) )
9 6 8 rspc ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 ) )
10 1 9 mpan9 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ∈ 𝐵 )
11 nfcv ⊢ Ⅎ 𝑧 𝑅
12 11 5 7 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 )
13 2 12 eqtrdi ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 ) )
14 nfcv ⊢ Ⅎ 𝑤 𝑆
15 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝑆
16 csbeq1a ⊢ ( 𝑦 = 𝑤 → 𝑆 = ⦋ 𝑤 / 𝑦 ⦌ 𝑆 )
17 14 15 16 cbvmpt ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = ( 𝑤 ∈ 𝐵 ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑆 )
18 3 17 eqtrdi ⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐵 ↦ ⦋ 𝑤 / 𝑦 ⦌ 𝑆 ) )
19 csbeq1 ⊢ ( 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑅 → ⦋ 𝑤 / 𝑦 ⦌ 𝑆 = ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
20 10 13 18 19 fmptco ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 ) )
21 nfcv ⊢ Ⅎ 𝑧 ⦋ 𝑅 / 𝑦 ⦌ 𝑆
22 nfcv ⊢ Ⅎ 𝑥 𝑆
23 5 22 nfcsbw ⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆
24 7 csbeq1d ⊢ ( 𝑥 = 𝑧 → ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
25 21 23 24 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑧 ∈ 𝐴 ↦ ⦋ ⦋ 𝑧 / 𝑥 ⦌ 𝑅 / 𝑦 ⦌ 𝑆 )
26 20 25 eqtr4di ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) )
27 eqid ⊢ 𝐴 = 𝐴
28 nfcvd ⊢ ( 𝑅 ∈ 𝐵 → Ⅎ 𝑦 𝑇 )
29 28 4 csbiegf ⊢ ( 𝑅 ∈ 𝐵 → ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 )
30 29 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 )
31 mpteq12 ⊢ ( ( 𝐴 = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ⦋ 𝑅 / 𝑦 ⦌ 𝑆 = 𝑇 ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
32 27 30 31 sylancr ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
33 1 32 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑅 / 𝑦 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
34 26 33 eqtrd ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )