hdmap1cbv

Description: Frequently used lemma to change bound variables in L hypothesis. (Contributed by NM, 15-May-2015)

		Ref	Expression
	Hypothesis	hdmap1cbv.l	⊢ 𝐿 = ( 𝑥 ∈ V ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
	Assertion	hdmap1cbv	⊢ 𝐿 = ( 𝑦 ∈ V ↦ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1cbv.l	⊢ 𝐿 = ( 𝑥 ∈ V ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
2		fveq2	⊢ ( 𝑥 = 𝑦 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) )
3	2	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 2^nd ‘ 𝑥 ) = 0 ↔ ( 2^nd ‘ 𝑦 ) = 0 ) )
4	2	sneqd	⊢ ( 𝑥 = 𝑦 → { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ 𝑦 ) } )
5	4	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) = ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) )
6	5	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) )
7	6	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ) )
8		2fveq3	⊢ ( 𝑥 = 𝑦 → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) )
9	8 2	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) )
10	9	sneqd	⊢ ( 𝑥 = 𝑦 → { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } = { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } )
11	10	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) = ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) )
12	11	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) )
13		2fveq3	⊢ ( 𝑥 = 𝑦 → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) )
14	13	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) )
15	14	sneqd	⊢ ( 𝑥 = 𝑦 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } )
16	15	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) )
17	12 16	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) )
18	7 17	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) )
19	18	riotabidv	⊢ ( 𝑥 = 𝑦 → ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) )
20	3 19	ifbieq2d	⊢ ( 𝑥 = 𝑦 → if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) ) )
21	20	cbvmptv	⊢ ( 𝑥 ∈ V ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) = ( 𝑦 ∈ V ↦ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) ) )
22		sneq	⊢ ( ℎ = 𝑖 → { ℎ } = { 𝑖 } )
23	22	fveq2d	⊢ ( ℎ = 𝑖 → ( 𝐽 ‘ { ℎ } ) = ( 𝐽 ‘ { 𝑖 } ) )
24	23	eqeq2d	⊢ ( ℎ = 𝑖 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ) )
25		oveq2	⊢ ( ℎ = 𝑖 → ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) )
26	25	sneqd	⊢ ( ℎ = 𝑖 → { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } )
27	26	fveq2d	⊢ ( ℎ = 𝑖 → ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) )
28	27	eqeq2d	⊢ ( ℎ = 𝑖 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) )
29	24 28	anbi12d	⊢ ( ℎ = 𝑖 → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) )
30	29	cbvriotavw	⊢ ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) )
31		ifeq2	⊢ ( ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) → if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) ) )
32	30 31	ax-mp	⊢ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) )
33	32	mpteq2i	⊢ ( 𝑦 ∈ V ↦ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 ℎ ) } ) ) ) ) ) = ( 𝑦 ∈ V ↦ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) ) )
34	1 21 33	3eqtri	⊢ 𝐿 = ( 𝑦 ∈ V ↦ if ( ( 2^nd ‘ 𝑦 ) = 0 , 𝑄 , ( ℩ 𝑖 ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑦 ) } ) ) = ( 𝐽 ‘ { 𝑖 } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) − ( 2^nd ‘ 𝑦 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) 𝑅 𝑖 ) } ) ) ) ) )

Metamath Proof Explorer

Theorem hdmap1cbv

Proof