# Metamath Proof Explorer

## Theorem dmmpossx

Description: The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypothesis fmpox.1 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
Assertion dmmpossx dom 𝐹 𝑥𝐴 ( { 𝑥 } × 𝐵 )

### Proof

Step Hyp Ref Expression
1 fmpox.1 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
2 nfcv 𝑢 𝐵
3 nfcsb1v 𝑥 𝑢 / 𝑥 𝐵
4 nfcv 𝑢 𝐶
5 nfcv 𝑣 𝐶
6 nfcsb1v 𝑥 𝑢 / 𝑥 𝑣 / 𝑦 𝐶
7 nfcv 𝑦 𝑢
8 nfcsb1v 𝑦 𝑣 / 𝑦 𝐶
9 7 8 nfcsbw 𝑦 𝑢 / 𝑥 𝑣 / 𝑦 𝐶
10 csbeq1a ( 𝑥 = 𝑢𝐵 = 𝑢 / 𝑥 𝐵 )
11 csbeq1a ( 𝑦 = 𝑣𝐶 = 𝑣 / 𝑦 𝐶 )
12 csbeq1a ( 𝑥 = 𝑢 𝑣 / 𝑦 𝐶 = 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
13 11 12 sylan9eqr ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → 𝐶 = 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
14 2 3 4 5 6 9 10 13 cbvmpox ( 𝑥𝐴 , 𝑦𝐵𝐶 ) = ( 𝑢𝐴 , 𝑣 𝑢 / 𝑥 𝐵 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
15 vex 𝑢 ∈ V
16 vex 𝑣 ∈ V
17 15 16 op1std ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st𝑡 ) = 𝑢 )
18 17 csbeq1d ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st𝑡 ) / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 = 𝑢 / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 )
19 15 16 op2ndd ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd𝑡 ) = 𝑣 )
20 19 csbeq1d ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd𝑡 ) / 𝑦 𝐶 = 𝑣 / 𝑦 𝐶 )
21 20 csbeq2dv ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → 𝑢 / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 = 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
22 18 21 eqtrd ( 𝑡 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st𝑡 ) / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 = 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
23 22 mpomptx ( 𝑡 𝑢𝐴 ( { 𝑢 } × 𝑢 / 𝑥 𝐵 ) ↦ ( 1st𝑡 ) / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 ) = ( 𝑢𝐴 , 𝑣 𝑢 / 𝑥 𝐵 𝑢 / 𝑥 𝑣 / 𝑦 𝐶 )
24 14 1 23 3eqtr4i 𝐹 = ( 𝑡 𝑢𝐴 ( { 𝑢 } × 𝑢 / 𝑥 𝐵 ) ↦ ( 1st𝑡 ) / 𝑥 ( 2nd𝑡 ) / 𝑦 𝐶 )
25 24 dmmptss dom 𝐹 𝑢𝐴 ( { 𝑢 } × 𝑢 / 𝑥 𝐵 )
26 nfcv 𝑢 ( { 𝑥 } × 𝐵 )
27 nfcv 𝑥 { 𝑢 }
28 27 3 nfxp 𝑥 ( { 𝑢 } × 𝑢 / 𝑥 𝐵 )
29 sneq ( 𝑥 = 𝑢 → { 𝑥 } = { 𝑢 } )
30 29 10 xpeq12d ( 𝑥 = 𝑢 → ( { 𝑥 } × 𝐵 ) = ( { 𝑢 } × 𝑢 / 𝑥 𝐵 ) )
31 26 28 30 cbviun 𝑥𝐴 ( { 𝑥 } × 𝐵 ) = 𝑢𝐴 ( { 𝑢 } × 𝑢 / 𝑥 𝐵 )
32 25 31 sseqtrri dom 𝐹 𝑥𝐴 ( { 𝑥 } × 𝐵 )