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

Theorem fpwwelem 10639
Description: Lemma for fpwwe 10640. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
Hypotheses
Ref Expression
fpwwe.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
fpwwe.2 (𝜑𝐴𝑉)
Assertion
Ref Expression
fpwwelem (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))))
Distinct variable groups:   𝑥,𝑟,𝐴   𝑦,𝑟,𝐹,𝑥   𝜑,𝑟,𝑥,𝑦   𝑅,𝑟,𝑥,𝑦   𝑋,𝑟,𝑥,𝑦   𝑊,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝑉(𝑥,𝑦,𝑟)

Proof of Theorem fpwwelem
StepHypRef Expression
1 fpwwe.1 . . . . 5 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
21relopabiv 5820 . . . 4 Rel 𝑊
32a1i 11 . . 3 (𝜑 → Rel 𝑊)
4 brrelex12 5728 . . 3 ((Rel 𝑊𝑋𝑊𝑅) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
53, 4sylan 580 . 2 ((𝜑𝑋𝑊𝑅) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
6 fpwwe.2 . . . . 5 (𝜑𝐴𝑉)
76adantr 481 . . . 4 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → 𝐴𝑉)
8 simprll 777 . . . 4 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → 𝑋𝐴)
97, 8ssexd 5324 . . 3 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → 𝑋 ∈ V)
109, 9xpexd 7737 . . . 4 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → (𝑋 × 𝑋) ∈ V)
11 simprlr 778 . . . 4 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → 𝑅 ⊆ (𝑋 × 𝑋))
1210, 11ssexd 5324 . . 3 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → 𝑅 ∈ V)
139, 12jca 512 . 2 ((𝜑 ∧ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
14 simpl 483 . . . . . 6 ((𝑥 = 𝑋𝑟 = 𝑅) → 𝑥 = 𝑋)
1514sseq1d 4013 . . . . 5 ((𝑥 = 𝑋𝑟 = 𝑅) → (𝑥𝐴𝑋𝐴))
16 simpr 485 . . . . . 6 ((𝑥 = 𝑋𝑟 = 𝑅) → 𝑟 = 𝑅)
1714sqxpeqd 5708 . . . . . 6 ((𝑥 = 𝑋𝑟 = 𝑅) → (𝑥 × 𝑥) = (𝑋 × 𝑋))
1816, 17sseq12d 4015 . . . . 5 ((𝑥 = 𝑋𝑟 = 𝑅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑅 ⊆ (𝑋 × 𝑋)))
1915, 18anbi12d 631 . . . 4 ((𝑥 = 𝑋𝑟 = 𝑅) → ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ↔ (𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋))))
20 weeq2 5665 . . . . . 6 (𝑥 = 𝑋 → (𝑟 We 𝑥𝑟 We 𝑋))
21 weeq1 5664 . . . . . 6 (𝑟 = 𝑅 → (𝑟 We 𝑋𝑅 We 𝑋))
2220, 21sylan9bb 510 . . . . 5 ((𝑥 = 𝑋𝑟 = 𝑅) → (𝑟 We 𝑥𝑅 We 𝑋))
2316cnveqd 5875 . . . . . . . 8 ((𝑥 = 𝑋𝑟 = 𝑅) → 𝑟 = 𝑅)
2423imaeq1d 6058 . . . . . . 7 ((𝑥 = 𝑋𝑟 = 𝑅) → (𝑟 “ {𝑦}) = (𝑅 “ {𝑦}))
2524fveqeq2d 6899 . . . . . 6 ((𝑥 = 𝑋𝑟 = 𝑅) → ((𝐹‘(𝑟 “ {𝑦})) = 𝑦 ↔ (𝐹‘(𝑅 “ {𝑦})) = 𝑦))
2614, 25raleqbidv 3342 . . . . 5 ((𝑥 = 𝑋𝑟 = 𝑅) → (∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦 ↔ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))
2722, 26anbi12d 631 . . . 4 ((𝑥 = 𝑋𝑟 = 𝑅) → ((𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦) ↔ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦)))
2819, 27anbi12d 631 . . 3 ((𝑥 = 𝑋𝑟 = 𝑅) → (((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦)) ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))))
2928, 1brabga 5534 . 2 ((𝑋 ∈ V ∧ 𝑅 ∈ V) → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))))
305, 13, 29pm5.21nd 800 1 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 (𝐹‘(𝑅 “ {𝑦})) = 𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  Vcvv 3474  wss 3948  {csn 4628   class class class wbr 5148  {copab 5210   We wwe 5630   × cxp 5674  ccnv 5675  cima 5679  Rel wrel 5681  cfv 6543
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 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fv 6551
This theorem is referenced by:  canth4  10641  canthnumlem  10642  canthp1lem2  10647
  Copyright terms: Public domain W3C validator