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 36110
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 6103 . . . . 5 (𝑥 = 𝑦 → (2nd𝑥) = (2nd𝑦))
32eqeq1d 2612 . . . 4 (𝑥 = 𝑦 → ((2nd𝑥) = 0 ↔ (2nd𝑦) = 0 ))
42sneqd 4137 . . . . . . . . 9 (𝑥 = 𝑦 → {(2nd𝑥)} = {(2nd𝑦)})
54fveq2d 6107 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{(2nd𝑥)}) = (𝑁‘{(2nd𝑦)}))
65fveq2d 6107 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd𝑥)})) = (𝑀‘(𝑁‘{(2nd𝑦)})))
76eqeq1d 2612 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{})))
8 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (1st𝑥) = (1st𝑦))
98fveq2d 6107 . . . . . . . . . . 11 (𝑥 = 𝑦 → (1st ‘(1st𝑥)) = (1st ‘(1st𝑦)))
109, 2oveq12d 6567 . . . . . . . . . 10 (𝑥 = 𝑦 → ((1st ‘(1st𝑥)) (2nd𝑥)) = ((1st ‘(1st𝑦)) (2nd𝑦)))
1110sneqd 4137 . . . . . . . . 9 (𝑥 = 𝑦 → {((1st ‘(1st𝑥)) (2nd𝑥))} = {((1st ‘(1st𝑦)) (2nd𝑦))})
1211fveq2d 6107 . . . . . . . 8 (𝑥 = 𝑦 → (𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))}) = (𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))}))
1312fveq2d 6107 . . . . . . 7 (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})))
148fveq2d 6107 . . . . . . . . . 10 (𝑥 = 𝑦 → (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)))
1514oveq1d 6564 . . . . . . . . 9 (𝑥 = 𝑦 → ((2nd ‘(1st𝑥))𝑅) = ((2nd ‘(1st𝑦))𝑅))
1615sneqd 4137 . . . . . . . 8 (𝑥 = 𝑦 → {((2nd ‘(1st𝑥))𝑅)} = {((2nd ‘(1st𝑦))𝑅)})
1716fveq2d 6107 . . . . . . 7 (𝑥 = 𝑦 → (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))
1813, 17eqeq12d 2625 . . . . . 6 (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))
197, 18anbi12d 743 . . . . 5 (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
2019riotabidv 6513 . . . 4 (𝑥 = 𝑦 → (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))) = (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))
213, 20ifbieq2d 4061 . . 3 (𝑥 = 𝑦 → if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
2221cbvmptv 4678 . 2 (𝑥 ∈ V ↦ if((2nd𝑥) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑥)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑥)) (2nd𝑥))})) = (𝐽‘{((2nd ‘(1st𝑥))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))))
23 sneq 4135 . . . . . . . 8 ( = 𝑖 → {} = {𝑖})
2423fveq2d 6107 . . . . . . 7 ( = 𝑖 → (𝐽‘{}) = (𝐽‘{𝑖}))
2524eqeq2d 2620 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ↔ (𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖})))
26 oveq2 6557 . . . . . . . . 9 ( = 𝑖 → ((2nd ‘(1st𝑦))𝑅) = ((2nd ‘(1st𝑦))𝑅𝑖))
2726sneqd 4137 . . . . . . . 8 ( = 𝑖 → {((2nd ‘(1st𝑦))𝑅)} = {((2nd ‘(1st𝑦))𝑅𝑖)})
2827fveq2d 6107 . . . . . . 7 ( = 𝑖 → (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))
2928eqeq2d 2620 . . . . . 6 ( = 𝑖 → ((𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}) ↔ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
3025, 29anbi12d 743 . . . . 5 ( = 𝑖 → (((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})) ↔ ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3130cbvriotav 6522 . . . 4 (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))) = (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))
32 ifeq2 4041 . . . 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𝑦))𝑅𝑖)})))))
3331, 32ax-mp 5 . . 3 if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)})))) = if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)}))))
3433mpteq2i 4669 . 2 (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅)}))))) = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
351, 22, 343eqtri 2636 1 𝐿 = (𝑦 ∈ V ↦ if((2nd𝑦) = 0 , 𝑄, (𝑖𝐷 ((𝑀‘(𝑁‘{(2nd𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st𝑦)) (2nd𝑦))})) = (𝐽‘{((2nd ‘(1st𝑦))𝑅𝑖)})))))
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1475  Vcvv 3173  ifcif 4036  {csn 4125  cmpt 4643  cfv 5804  crio 6510  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-iota 5768  df-fv 5812  df-riota 6511  df-ov 6552
This theorem is referenced by:  hdmap1valc  36111  hdmap1eu  36133  hdmap1euOLDN  36134
  Copyright terms: Public domain W3C validator