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

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 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )