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 42050
 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 4334, which is not an element of all unordered pairs, see spr0nelg 42051. (Contributed by AV, 21-Nov-2021.)
Assertion
Ref Expression
elsprel ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}})
Distinct variable groups:   𝐴,𝑎,𝑏,𝑝   𝐵,𝑎,𝑏,𝑝
Allowed substitution hints:   𝑉(𝑝,𝑎,𝑏)   𝑊(𝑝,𝑎,𝑏)

Proof of Theorem elsprel
StepHypRef Expression
1 elex 3243 . . . 4 (𝐴𝑉𝐴 ∈ V)
2 elex 3243 . . . 4 (𝐵𝑊𝐵 ∈ V)
31, 2orim12i 537 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4 elisset 3246 . . . . . . 7 (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5 elisset 3246 . . . . . . 7 (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6 eeanv 2218 . . . . . . . 8 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7 preq12 4302 . . . . . . . . . 10 ((𝑎 = 𝐴𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
87eqcomd 2657 . . . . . . . . 9 ((𝑎 = 𝐴𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
982eximi 1803 . . . . . . . 8 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = 𝐵) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
106, 9sylbir 225 . . . . . . 7 ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
114, 5, 10syl2an 493 . . . . . 6 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
1211expcom 450 . . . . 5 (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13 preq2 4301 . . . . . . . . . . . . . 14 (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
1413adantr 480 . . . . . . . . . . . . 13 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15 dfsn2 4223 . . . . . . . . . . . . . 14 {𝑎} = {𝑎, 𝑎}
16 sneq 4220 . . . . . . . . . . . . . . 15 (𝑎 = 𝐴 → {𝑎} = {𝐴})
1716adantl 481 . . . . . . . . . . . . . 14 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎} = {𝐴})
1815, 17syl5eqr 2699 . . . . . . . . . . . . 13 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
1914, 18eqtr2d 2686 . . . . . . . . . . . 12 ((𝑏 = 𝑎𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
2019ex 449 . . . . . . . . . . 11 (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
2120spimev 2295 . . . . . . . . . 10 (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
2221adantl 481 . . . . . . . . 9 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23 prprc2 4333 . . . . . . . . . . . 12 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
2423adantr 480 . . . . . . . . . . 11 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
2524eqeq1d 2653 . . . . . . . . . 10 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
2625exbidv 1890 . . . . . . . . 9 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
2722, 26mpbird 247 . . . . . . . 8 ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
2827ex 449 . . . . . . 7 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
2928eximdv 1886 . . . . . 6 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
304, 29syl5 34 . . . . 5 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
3112, 30pm2.61i 176 . . . 4 (𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
3211ex 449 . . . . 5 (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33 preq1 4300 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
3433adantr 480 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35 dfsn2 4223 . . . . . . . . . . . . . . . . 17 {𝑏} = {𝑏, 𝑏}
36 sneq 4220 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐵 → {𝑏} = {𝐵})
3736adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑏} = {𝐵})
3835, 37syl5eqr 2699 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
3934, 38eqtr2d 2686 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑏𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
4039ex 449 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
4140spimev 2295 . . . . . . . . . . . . 13 (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
4241adantl 481 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43 prprc1 4332 . . . . . . . . . . . . . . 15 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
4443adantr 480 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
4544eqeq1d 2653 . . . . . . . . . . . . 13 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
4645exbidv 1890 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
4742, 46mpbird 247 . . . . . . . . . . 11 ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
4847ex 449 . . . . . . . . . 10 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
4948eximdv 1886 . . . . . . . . 9 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
5049impcom 445 . . . . . . . 8 ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51 excom 2082 . . . . . . . 8 (∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
5250, 51sylibr 224 . . . . . . 7 ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
5352ex 449 . . . . . 6 (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
5453, 5syl11 33 . . . . 5 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
5532, 54pm2.61i 176 . . . 4 (𝐵 ∈ V → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
5631, 55jaoi 393 . . 3 ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
573, 56syl 17 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58 prex 4939 . . 3 {𝐴, 𝐵} ∈ V
59 eqeq1 2655 . . . 4 (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60592exbidv 1892 . . 3 (𝑝 = {𝐴, 𝐵} → (∃𝑎𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
6158, 60elab 3382 . 2 ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
6257, 61sylibr 224 1 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎𝑏 𝑝 = {𝑎, 𝑏}})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637  Vcvv 3231  {csn 4210  {cpr 4212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-nul 3949  df-sn 4211  df-pr 4213 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator