Theorem elsprel 47456

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 4748, which is not an element of all unordered pairs, see spr0nelg 47457. (Contributed by AV, 21-Nov-2021.)

Assertion

Ref	Expression
elsprel	⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Distinct variable groups:   𝐴,𝑎,𝑏,𝑝   𝐵,𝑎,𝑏,𝑝

Allowed substitution hints:   𝑉(𝑝,𝑎,𝑏)   𝑊(𝑝,𝑎,𝑏)

Proof of Theorem elsprel

Step	Hyp	Ref	Expression
1		elex 3485	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3485	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3	1, 2	orim12i 908	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4		elisset 2817	. . . . . . 7 ⊢ (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5		elisset 2817	. . . . . . 7 ⊢ (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6		exdistrv 1955	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7		preq12 4716	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
8	7	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
9	8	2eximi 1836	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
10	6, 9	sylbir 235	. . . . . . 7 ⊢ ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
11	4, 5, 10	syl2an 596	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
12	11	expcom 413	. . . . 5 ⊢ (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13		preq2 4715	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
14	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15		dfsn2 4619	. . . . . . . . . . . . . 14 ⊢ {𝑎} = {𝑎, 𝑎}
16		sneq 4616	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
17	16	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎} = {𝐴})
18	15, 17	eqtr3id 2785	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
19	14, 18	eqtr2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
20	19	ex 412	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
21	20	spimevw 1985	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
22	21	adantl 481	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23		prprc2 4747	. . . . . . . . . . . 12 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
24	23	adantr 480	. . . . . . . . . . 11 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2738	. . . . . . . . . 10 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
26	25	exbidv 1921	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
27	22, 26	mpbird 257	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
28	27	ex 412	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
29	28	eximdv 1917	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
30	4, 29	syl5 34	. . . . 5 ⊢ (¬ 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
31	12, 30	pm2.61i 182	. . . 4 ⊢ (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
32	11	ex 412	. . . . 5 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33		preq1 4714	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
34	33	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35		dfsn2 4619	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} = {𝑏, 𝑏}
36		sneq 4616	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
37	36	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏} = {𝐵})
38	35, 37	eqtr3id 2785	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
39	34, 38	eqtr2d 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
40	39	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
41	40	spimevw 1985	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
42	41	adantl 481	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43		prprc1 4746	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
44	43	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
45	44	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
46	45	exbidv 1921	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
47	42, 46	mpbird 257	. . . . . . . . . . 11 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
48	47	ex 412	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
49	48	eximdv 1917	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
50	49	impcom 407	. . . . . . . 8 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51		excom 2163	. . . . . . . 8 ⊢ (∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
52	50, 51	sylibr 234	. . . . . . 7 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
53	52	ex 412	. . . . . 6 ⊢ (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
54	53, 5	syl11 33	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
55	32, 54	pm2.61i 182	. . . 4 ⊢ (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
56	31, 55	jaoi 857	. . 3 ⊢ ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
57	3, 56	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58		prex 5412	. . 3 ⊢ {𝐴, 𝐵} ∈ V
59		eqeq1 2740	. . . 4 ⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60	59	2exbidv 1924	. . 3 ⊢ (𝑝 = {𝐴, 𝐵} → (∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
61	58, 60	elab 3663	. 2 ⊢ ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
62	57, 61	sylibr 234	1 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714  Vcvv 3464  {csn 4606  {cpr 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-un 3936  df-nul 4314  df-sn 4607  df-pr 4609

This theorem is referenced by: (None)