Theorem elsprel 44815

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 4700, which is not an element of all unordered pairs, see spr0nelg 44816. (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 3440	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3440	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3	1, 2	orim12i 905	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4		elisset 2820	. . . . . . 7 ⊢ (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5		elisset 2820	. . . . . . 7 ⊢ (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6		exdistrv 1960	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7		preq12 4668	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
8	7	eqcomd 2744	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
9	8	2eximi 1839	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
10	6, 9	sylbir 234	. . . . . . 7 ⊢ ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
11	4, 5, 10	syl2an 595	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
12	11	expcom 413	. . . . 5 ⊢ (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13		preq2 4667	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
14	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15		dfsn2 4571	. . . . . . . . . . . . . 14 ⊢ {𝑎} = {𝑎, 𝑎}
16		sneq 4568	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
17	16	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎} = {𝐴})
18	15, 17	eqtr3id 2793	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
19	14, 18	eqtr2d 2779	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
20	19	ex 412	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
21	20	spimevw 1999	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
22	21	adantl 481	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23		prprc2 4699	. . . . . . . . . . . 12 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
24	23	adantr 480	. . . . . . . . . . 11 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2740	. . . . . . . . . 10 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
26	25	exbidv 1925	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
27	22, 26	mpbird 256	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
28	27	ex 412	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
29	28	eximdv 1921	. . . . . 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 4666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
34	33	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35		dfsn2 4571	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} = {𝑏, 𝑏}
36		sneq 4568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
37	36	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏} = {𝐵})
38	35, 37	eqtr3id 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
39	34, 38	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
40	39	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
41	40	spimevw 1999	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
42	41	adantl 481	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43		prprc1 4698	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
44	43	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
45	44	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
46	45	exbidv 1925	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
47	42, 46	mpbird 256	. . . . . . . . . . 11 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
48	47	ex 412	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
49	48	eximdv 1921	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
50	49	impcom 407	. . . . . . . 8 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51		excom 2164	. . . . . . . 8 ⊢ (∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
52	50, 51	sylibr 233	. . . . . . 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 853	. . 3 ⊢ ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
57	3, 56	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58		prex 5350	. . 3 ⊢ {𝐴, 𝐵} ∈ V
59		eqeq1 2742	. . . 4 ⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60	59	2exbidv 1928	. . 3 ⊢ (𝑝 = {𝐴, 𝐵} → (∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
61	58, 60	elab 3602	. 2 ⊢ ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
62	57, 61	sylibr 233	1 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  Vcvv 3422  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-pr 4561

This theorem is referenced by: (None)