Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elsprel Structured version   Visualization version   GIF version

Theorem elsprel 44388
 Description: An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc 4663, which is not an element of all unordered pairs, see spr0nelg 44389. (Contributed by AV, 21-Nov-2021.)
Assertion
Ref Expression
elsprel ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}})
Distinct variable groups:   𝐴,𝑎,𝑏,𝑝   𝐵,𝑎,𝑏,𝑝
Allowed substitution hints:   𝑉(𝑝,𝑎,𝑏)   𝑊(𝑝,𝑎,𝑏)

Proof of Theorem elsprel
StepHypRef Expression
1 elex 3428 . . . 4 (𝐴𝑉𝐴 ∈ V)
2 elex 3428 . . . 4 (𝐵𝑊𝐵 ∈ V)
31, 2orim12i 906 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4 elisset 2833 . . . . . . 7 (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5 elisset 2833 . . . . . . 7 (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6 exdistrv 1956 . . . . . . . 8 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7 preq12 4631 . . . . . . . . . 10 ((𝑎 = 𝐴𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
87eqcomd 2764 . . . . . . . . 9 ((𝑎 = 𝐴𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
982eximi 1837 . . . . . . . 8 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = 𝐵) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
106, 9sylbir 238 . . . . . . 7 ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
114, 5, 10syl2an 598 . . . . . 6 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
1211expcom 417 . . . . 5 (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13 preq2 4630 . . . . . . . . . . . . . 14 (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
1413adantr 484 . . . . . . . . . . . . 13 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15 dfsn2 4538 . . . . . . . . . . . . . 14 {𝑎} = {𝑎, 𝑎}
16 sneq 4535 . . . . . . . . . . . . . . 15 (𝑎 = 𝐴 → {𝑎} = {𝐴})
1716adantl 485 . . . . . . . . . . . . . 14 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎} = {𝐴})
1815, 17syl5eqr 2807 . . . . . . . . . . . . 13 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
1914, 18eqtr2d 2794 . . . . . . . . . . . 12 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
2019ex 416 . . . . . . . . . . 11 (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
2120spimevw 2001 . . . . . . . . . 10 (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
2221adantl 485 . . . . . . . . 9 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23 prprc2 4662 . . . . . . . . . . . 12 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
2423adantr 484 . . . . . . . . . . 11 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
2524eqeq1d 2760 . . . . . . . . . 10 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
2625exbidv 1922 . . . . . . . . 9 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
2722, 26mpbird 260 . . . . . . . 8 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
2827ex 416 . . . . . . 7 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
2928eximdv 1918 . . . . . 6 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
304, 29syl5 34 . . . . 5 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
3112, 30pm2.61i 185 . . . 4 (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
3211ex 416 . . . . 5 (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33 preq1 4629 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
3433adantr 484 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35 dfsn2 4538 . . . . . . . . . . . . . . . . 17 {𝑏} = {𝑏, 𝑏}
36 sneq 4535 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐵 → {𝑏} = {𝐵})
3736adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑏} = {𝐵})
3835, 37syl5eqr 2807 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
3934, 38eqtr2d 2794 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
4039ex 416 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
4140spimevw 2001 . . . . . . . . . . . . 13 (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
4241adantl 485 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43 prprc1 4661 . . . . . . . . . . . . . . 15 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
4443adantr 484 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
4544eqeq1d 2760 . . . . . . . . . . . . 13 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
4645exbidv 1922 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
4742, 46mpbird 260 . . . . . . . . . . 11 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
4847ex 416 . . . . . . . . . 10 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
4948eximdv 1918 . . . . . . . . 9 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
5049impcom 411 . . . . . . . 8 ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51 excom 2166 . . . . . . . 8 (∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
5250, 51sylibr 237 . . . . . . 7 ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
5352ex 416 . . . . . 6 (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
5453, 5syl11 33 . . . . 5 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
5532, 54pm2.61i 185 . . . 4 (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
5631, 55jaoi 854 . . 3 ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
573, 56syl 17 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58 prex 5304 . . 3 {𝐴, 𝐵} ∈ V
59 eqeq1 2762 . . . 4 (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60592exbidv 1925 . . 3 (𝑝 = {𝐴, 𝐵} → (∃𝑎𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
6158, 60elab 3590 . 2 ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
6257, 61sylibr 237 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2735  Vcvv 3409  {csn 4525  {cpr 4527 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-v 3411  df-dif 3863  df-un 3865  df-nul 4228  df-sn 4526  df-pr 4528 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator