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 ( 𝜑 → ( 𝐺𝐹 ) = ( 𝑥𝐴𝑇 ) )