Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

	Ref	Expression
Hypotheses	elovmporab.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } )
	elovmporab.v	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑀 ∈ V )
Assertion	elovmporab	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elovmporab.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } )
2		elovmporab.v	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑀 ∈ V )
3	1	elmpocl	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
4	1	a1i	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ 𝑀 ∣ 𝜑 } ) )
5		sbceq1a	⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
6		sbceq1a	⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
7	5 6	sylan9bbr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
8	7	adantl	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
9	8	rabbidv	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ 𝑀 ∣ 𝜑 } = { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
10		eqidd	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑥 = 𝑋 ) → V = V )
11		simpl	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑋 ∈ V )
12		simpr	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑌 ∈ V )
13		rabexg	⊢ ( 𝑀 ∈ V → { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
14	2 13	syl	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
15		nfcv	⊢ Ⅎ 𝑥 𝑋
16	15	nfel1	⊢ Ⅎ 𝑥 𝑋 ∈ V
17		nfcv	⊢ Ⅎ 𝑥 𝑌
18	17	nfel1	⊢ Ⅎ 𝑥 𝑌 ∈ V
19	16 18	nfan	⊢ Ⅎ 𝑥 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
20		nfcv	⊢ Ⅎ 𝑦 𝑋
21	20	nfel1	⊢ Ⅎ 𝑦 𝑋 ∈ V
22		nfcv	⊢ Ⅎ 𝑦 𝑌
23	22	nfel1	⊢ Ⅎ 𝑦 𝑌 ∈ V
24	21 23	nfan	⊢ Ⅎ 𝑦 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
25		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
26		nfcv	⊢ Ⅎ 𝑥 𝑀
27	25 26	nfrabw	⊢ Ⅎ 𝑥 { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
28		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑
29	20 28	nfsbcw	⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
30		nfcv	⊢ Ⅎ 𝑦 𝑀
31	29 30	nfrabw	⊢ Ⅎ 𝑦 { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
32	4 9 10 11 12 14 19 24 20 17 27 31	ovmpodxf	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
33	32	eleq2d	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
34		df-3an	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ 𝑀 ) )
35	34	simplbi2com	⊢ ( 𝑍 ∈ 𝑀 → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
36		elrabi	⊢ ( 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → 𝑍 ∈ 𝑀 )
37	35 36	syl11	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ { 𝑧 ∈ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
38	33 37	sylbid	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) ) )
39	3 38	mpcom	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀 ) )