MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2cbv Structured version   Visualization version   GIF version

Theorem fpwwe2cbv 10667
Description: Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 3-Jun-2015.)
Hypothesis
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
Assertion
Ref Expression
fpwwe2cbv 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
Distinct variable groups:   𝑦,𝑢   𝑟,𝑎,𝑠,𝑢,𝑣,𝑥,𝑦,𝑧,𝐹   𝐴,𝑎,𝑟,𝑠,𝑥,𝑧
Allowed substitution hints:   𝐴(𝑦,𝑣,𝑢)   𝑊(𝑥,𝑦,𝑧,𝑣,𝑢,𝑠,𝑟,𝑎)

Proof of Theorem fpwwe2cbv
StepHypRef Expression
1 fpwwe2.1 . 2 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
2 simpl 482 . . . . . 6 ((𝑥 = 𝑎𝑟 = 𝑠) → 𝑥 = 𝑎)
32sseq1d 4026 . . . . 5 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑥𝐴𝑎𝐴))
4 simpr 484 . . . . . 6 ((𝑥 = 𝑎𝑟 = 𝑠) → 𝑟 = 𝑠)
52sqxpeqd 5720 . . . . . 6 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑥 × 𝑥) = (𝑎 × 𝑎))
64, 5sseq12d 4028 . . . . 5 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑠 ⊆ (𝑎 × 𝑎)))
73, 6anbi12d 632 . . . 4 ((𝑥 = 𝑎𝑟 = 𝑠) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ↔ (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎))))
84, 2weeq12d 5677 . . . . 5 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑟 We 𝑥𝑠 We 𝑎))
9 id 22 . . . . . . . . . . 11 (𝑢 = 𝑣𝑢 = 𝑣)
109sqxpeqd 5720 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑢 × 𝑢) = (𝑣 × 𝑣))
1110ineq2d 4227 . . . . . . . . . . 11 (𝑢 = 𝑣 → (𝑟 ∩ (𝑢 × 𝑢)) = (𝑟 ∩ (𝑣 × 𝑣)))
129, 11oveq12d 7448 . . . . . . . . . 10 (𝑢 = 𝑣 → (𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))))
1312eqeq1d 2736 . . . . . . . . 9 (𝑢 = 𝑣 → ((𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦))
1413cbvsbcvw 3825 . . . . . . . 8 ([(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦[(𝑟 “ {𝑦}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦)
15 sneq 4640 . . . . . . . . . 10 (𝑦 = 𝑧 → {𝑦} = {𝑧})
1615imaeq2d 6079 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑟 “ {𝑦}) = (𝑟 “ {𝑧}))
17 eqeq2 2746 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦 ↔ (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧))
1816, 17sbceqbid 3797 . . . . . . . 8 (𝑦 = 𝑧 → ([(𝑟 “ {𝑦}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑦[(𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧))
1914, 18bitrid 283 . . . . . . 7 (𝑦 = 𝑧 → ([(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦[(𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧))
2019cbvralvw 3234 . . . . . 6 (∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑧𝑥 [(𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧)
214cnveqd 5888 . . . . . . . . 9 ((𝑥 = 𝑎𝑟 = 𝑠) → 𝑟 = 𝑠)
2221imaeq1d 6078 . . . . . . . 8 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑟 “ {𝑧}) = (𝑠 “ {𝑧}))
234ineq1d 4226 . . . . . . . . . 10 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑟 ∩ (𝑣 × 𝑣)) = (𝑠 ∩ (𝑣 × 𝑣)))
2423oveq2d 7446 . . . . . . . . 9 ((𝑥 = 𝑎𝑟 = 𝑠) → (𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = (𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))))
2524eqeq1d 2736 . . . . . . . 8 ((𝑥 = 𝑎𝑟 = 𝑠) → ((𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧 ↔ (𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))
2622, 25sbceqbid 3797 . . . . . . 7 ((𝑥 = 𝑎𝑟 = 𝑠) → ([(𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧[(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))
272, 26raleqbidv 3343 . . . . . 6 ((𝑥 = 𝑎𝑟 = 𝑠) → (∀𝑧𝑥 [(𝑟 “ {𝑧}) / 𝑣](𝑣𝐹(𝑟 ∩ (𝑣 × 𝑣))) = 𝑧 ↔ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))
2820, 27bitrid 283 . . . . 5 ((𝑥 = 𝑎𝑟 = 𝑠) → (∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))
298, 28anbi12d 632 . . . 4 ((𝑥 = 𝑎𝑟 = 𝑠) → ((𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧)))
307, 29anbi12d 632 . . 3 ((𝑥 = 𝑎𝑟 = 𝑠) → (((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))))
3130cbvopabv 5220 . 2 {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
321, 31eqtri 2762 1 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧𝑎 [(𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1536  wral 3058  [wsbc 3790  cin 3961  wss 3962  {csn 4630  {copab 5209   We wwe 5639   × cxp 5686  ccnv 5687  cima 5691  (class class class)co 7430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fv 6570  df-ov 7433
This theorem is referenced by:  fpwwe2lem11  10678  fpwwe2lem12  10679  canthwe  10688  pwfseqlem5  10700
  Copyright terms: Public domain W3C validator