Theorem fmpox

Description: Functionality, domain and codomain of a class given by the maps-to notation, where B ( x ) is not constant but depends on x . (Contributed by NM, 29-Dec-2014)

	Ref	Expression
Hypothesis	fmpox.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	fmpox	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fmpox.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		vex	⊢ 𝑧 ∈ V
3		vex	⊢ 𝑤 ∈ V
4	2 3	op1std	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 1st ‘ 𝑣 ) = 𝑧 )
5	4	csbeq1d	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 )
6	2 3	op2ndd	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑤 )
7	6	csbeq1d	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
8	7	csbeq2dv	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ 𝑧 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
9	5 8	eqtrd	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
10	9	eleq1d	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
11	10	raliunxp	⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
12		nfv	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 )
13		nfv	⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 )
14		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
15		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
16	15	nfcri	⊢ Ⅎ 𝑥 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵
17	14 16	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
18		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
19	18	nfeq2	⊢ Ⅎ 𝑥 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
20	17 19	nfan	⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
21		nfv	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
22		nfcv	⊢ Ⅎ 𝑦 𝑧
23		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶
24	22 23	nfcsbw	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
25	24	nfeq2	⊢ Ⅎ 𝑦 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶
26	21 25	nfan	⊢ Ⅎ 𝑦 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
27		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
28	27	adantr	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
29		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
30		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
31	30	eleq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
32	29 31	sylan9bbr	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
33	28 32	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
34		csbeq1a	⊢ ( 𝑦 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
35		csbeq1a	⊢ ( 𝑥 = 𝑧 → ⦋ 𝑤 / 𝑦 ⦌ 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
36	34 35	sylan9eqr	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
37	36	eqeq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑣 = 𝐶 ↔ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) )
38	33 37	anbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) ) )
39	12 13 20 26 38	cbvoprab12	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) }
40		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = 𝐶 ) }
41		df-mpo	⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑣 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ) }
42	39 40 41	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
43	9	mpomptx	⊢ ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 )
44	42 1 43	3eqtr4i	⊢ 𝐹 = ( 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 )
45	44	fmpt	⊢ ( ∀ 𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⦋ ( 1st ‘ 𝑣 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
46	11 45	bitr3i	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
47		nfv	⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷
48	18	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
49	15 48	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
50		nfv	⊢ Ⅎ 𝑤 𝐶 ∈ 𝐷
51	23	nfel1	⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷
52	34	eleq1d	⊢ ( 𝑦 = 𝑤 → ( 𝐶 ∈ 𝐷 ↔ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
53	50 51 52	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
54	35	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
55	30 54	raleqbidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
56	53 55	syl5bb	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 ) )
57	47 49 56	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ⦋ 𝑧 / 𝑥 ⦌ ⦋ 𝑤 / 𝑦 ⦌ 𝐶 ∈ 𝐷 )
58		nfcv	⊢ Ⅎ 𝑧 ( { 𝑥 } × 𝐵 )
59		nfcv	⊢ Ⅎ 𝑥 { 𝑧 }
60	59 15	nfxp	⊢ Ⅎ 𝑥 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
61		sneq	⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
62	61 30	xpeq12d	⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × 𝐵 ) = ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
63	58 60 62	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
64	63	feq2i	⊢ ( 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 ↔ 𝐹 : ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ⟶ 𝐷 )
65	46 57 64	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⟶ 𝐷 )