Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hdmap1cbv Structured version   Visualization version   GIF version

Theorem hdmap1cbv 40265
Description: Frequently used lemma to change bound variables in 𝐿 hypothesis. (Contributed by NM, 15-May-2015.)
Hypothesis
Ref Expression
hdmap1cbv.l 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
Assertion
Ref Expression
hdmap1cbv 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Distinct variable groups:   ,𝑖,𝑥,𝑦,𝐷   ,𝐽,𝑖,𝑥,𝑦   ,𝑀,𝑖,𝑥,𝑦   ,𝑁,𝑖,𝑥,𝑦   𝑥, 0 ,𝑦   𝑥,𝑄,𝑦   𝑅,,𝑖,𝑥,𝑦   ,,𝑖,𝑥,𝑦
Allowed substitution hints:   𝑄(,𝑖)   𝐿(𝑥,𝑦,,𝑖)   0 (,𝑖)

Proof of Theorem hdmap1cbv
StepHypRef Expression
1 hdmap1cbv.l . 2 𝐿 = (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))))
2 fveq2 6842 . . . . 5 (𝑥 = 𝑦 → (2nd𝑥) = (2nd𝑦))
32eqeq1d 2738 . . . 4 (𝑥 = 𝑦 → ((2nd𝑥) = 0 ↔ (2nd𝑦) = 0 ))
42sneqd 4598 . . . . . . . . 9 (𝑥 = 𝑦 → {(2nd𝑥)} = {(2nd𝑦)})
54fveq2d 6846 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{(2nd𝑥)}) = (𝑁‘{(2nd𝑦)}))
65fveq2d 6846 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd𝑥)})) = (𝑀‘(𝑁‘{(2nd𝑦)})))
76eqeq1d 2738 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{})))
8 2fveq3 6847 . . . . . . . . . . 11 (𝑥 = 𝑦 → (1st ‘(1st𝑥)) = (1st ‘(1st𝑦)))
98, 2oveq12d 7375 . . . . . . . . . 10 (𝑥 = 𝑦 → ((1st ‘(1st𝑥)) (2nd𝑥)) = ((1st ‘(1st𝑦)) (2nd𝑦)))
109sneqd 4598 . . . . . . . . 9 (𝑥 = 𝑦 → {((1st ‘(1st𝑥)) (2nd𝑥))} = {((1st ‘(1st𝑦)) (2nd𝑦))})
1110fveq2d 6846 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))}) = (𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))}))
1211fveq2d 6846 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})))
13 2fveq3 6847 . . . . . . . . . 10 (𝑥 = 𝑦 → (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)))
1413oveq1d 7372 . . . . . . . . 9 (𝑥 = 𝑦 → ((2nd ‘(1st𝑥))𝑅) = ((2nd ‘(1st𝑦))𝑅))
1514sneqd 4598 . . . . . . . 8 (𝑥 = 𝑦 → {((2nd ‘(1st𝑥))𝑅)} = {((2nd ‘(1st𝑦))𝑅)})
1615fveq2d 6846 . . . . . . 7 (𝑥 = 𝑦 → (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))
1712, 16eqeq12d 2752 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))
187, 17anbi12d 631 . . . . 5 (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
1918riotabidv 7315 . . . 4 (𝑥 = 𝑦 → (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
203, 19ifbieq2d 4512 . . 3 (𝑥 = 𝑦 → if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
2120cbvmptv 5218 . 2 (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
22 sneq 4596 . . . . . . . 8 ( = 𝑖 → {} = {𝑖})
2322fveq2d 6846 . . . . . . 7 ( = 𝑖 → (𝐽‘{}) = (𝐽‘{𝑖}))
2423eqeq2d 2747 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖})))
25 oveq2 7365 . . . . . . . . 9 ( = 𝑖 → ((2nd ‘(1st𝑦))𝑅) = ((2nd ‘(1st𝑦))𝑅𝑖))
2625sneqd 4598 . . . . . . . 8 ( = 𝑖 → {((2nd ‘(1st𝑦))𝑅)} = {((2nd ‘(1st𝑦))𝑅𝑖)})
2726fveq2d 6846 . . . . . . 7 ( = 𝑖 → (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))
2827eqeq2d 2747 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
2924, 28anbi12d 631 . . . . 5 ( = 𝑖 → (((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3029cbvriotavw 7323 . . . 4 (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
31 ifeq2 4491 . . . 4 ((𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))) → if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
3230, 31ax-mp 5 . . 3 if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3332mpteq2i 5210 . 2 (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
341, 21, 333eqtri 2768 1 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  Vcvv 3445  ifcif 4486  {csn 4586  cmpt 5188  cfv 6496  crio 7312  (class class class)co 7357  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-iota 6448  df-fv 6504  df-riota 7313  df-ov 7360
This theorem is referenced by:  hdmap1valc  40266  hdmap1eu  40287  hdmap1euOLDN  40288
  Copyright terms: Public domain W3C validator