Theorem dmmpossx2

Description: The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx . (Contributed by AV, 30-Mar-2019)

	Ref	Expression
Hypothesis	dmmpossx2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	dmmpossx2	⊢ dom 𝐹 ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )

Proof

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