ovmpt3rab1

Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
	ovmpt3rab1.m	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
	ovmpt3rab1.n	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
	ovmpt3rab1.p	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
	ovmpt3rab1.x	⊢ Ⅎ 𝑥 𝜓
	ovmpt3rab1.y	⊢ Ⅎ 𝑦 𝜓
Assertion	ovmpt3rab1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) )

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
2		ovmpt3rab1.m	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝐾 )
3		ovmpt3rab1.n	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝐿 )
4		ovmpt3rab1.p	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
5		ovmpt3rab1.x	⊢ Ⅎ 𝑥 𝜓
6		ovmpt3rab1.y	⊢ Ⅎ 𝑦 𝜓
7	1	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) ) )
8	3 4	rabeqbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑎 ∈ 𝑁 ∣ 𝜑 } = { 𝑎 ∈ 𝐿 ∣ 𝜓 } )
9	2 8	mpteq12dv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) )
10	9	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) )
11		eqidd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) ∧ 𝑥 = 𝑋 ) → V = V )
12		elex	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
13	12	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → 𝑋 ∈ V )
14		elex	⊢ ( 𝑌 ∈ 𝑊 → 𝑌 ∈ V )
15	14	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → 𝑌 ∈ V )
16		mptexg	⊢ ( 𝐾 ∈ 𝑈 → ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) ∈ V )
17	16	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) ∈ V )
18		nfv	⊢ Ⅎ 𝑥 ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 )
19		nfv	⊢ Ⅎ 𝑦 ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 )
20		nfcv	⊢ Ⅎ 𝑦 𝑋
21		nfcv	⊢ Ⅎ 𝑥 𝑌
22		nfcv	⊢ Ⅎ 𝑥 𝐾
23		nfcv	⊢ Ⅎ 𝑥 𝐿
24	5 23	nfrabw	⊢ Ⅎ 𝑥 { 𝑎 ∈ 𝐿 ∣ 𝜓 }
25	22 24	nfmpt	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } )
26		nfcv	⊢ Ⅎ 𝑦 𝐾
27		nfcv	⊢ Ⅎ 𝑦 𝐿
28	6 27	nfrabw	⊢ Ⅎ 𝑦 { 𝑎 ∈ 𝐿 ∣ 𝜓 }
29	26 28	nfmpt	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } )
30	7 10 11 13 15 17 18 19 20 21 25 29	ovmpodxf	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑧 ∈ 𝐾 ↦ { 𝑎 ∈ 𝐿 ∣ 𝜓 } ) )

Metamath Proof Explorer

Theorem ovmpt3rab1

Proof