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