Theorem elsprel 43644

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 4705, which is not an element of all unordered pairs, see spr0nelg 43645. (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 3514	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3514	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3	1, 2	orim12i 905	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4		elisset 3507	. . . . . . 7 ⊢ (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5		elisset 3507	. . . . . . 7 ⊢ (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6		exdistrv 1956	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7		preq12 4673	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
8	7	eqcomd 2829	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
9	8	2eximi 1836	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
10	6, 9	sylbir 237	. . . . . . 7 ⊢ ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
11	4, 5, 10	syl2an 597	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
12	11	expcom 416	. . . . 5 ⊢ (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13		preq2 4672	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
14	13	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15		dfsn2 4582	. . . . . . . . . . . . . 14 ⊢ {𝑎} = {𝑎, 𝑎}
16		sneq 4579	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
17	16	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎} = {𝐴})
18	15, 17	syl5eqr 2872	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
19	14, 18	eqtr2d 2859	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
20	19	ex 415	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
21	20	spimevw 2001	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
22	21	adantl 484	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23		prprc2 4704	. . . . . . . . . . . 12 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
24	23	adantr 483	. . . . . . . . . . 11 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2825	. . . . . . . . . 10 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
26	25	exbidv 1922	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
27	22, 26	mpbird 259	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
28	27	ex 415	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
29	28	eximdv 1918	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
30	4, 29	syl5 34	. . . . 5 ⊢ (¬ 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
31	12, 30	pm2.61i 184	. . . 4 ⊢ (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
32	11	ex 415	. . . . 5 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33		preq1 4671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
34	33	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35		dfsn2 4582	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} = {𝑏, 𝑏}
36		sneq 4579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
37	36	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏} = {𝐵})
38	35, 37	syl5eqr 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
39	34, 38	eqtr2d 2859	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
40	39	ex 415	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
41	40	spimevw 2001	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
42	41	adantl 484	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43		prprc1 4703	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
44	43	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
45	44	eqeq1d 2825	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
46	45	exbidv 1922	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
47	42, 46	mpbird 259	. . . . . . . . . . 11 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
48	47	ex 415	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
49	48	eximdv 1918	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
50	49	impcom 410	. . . . . . . 8 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51		excom 2169	. . . . . . . 8 ⊢ (∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
52	50, 51	sylibr 236	. . . . . . 7 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
53	52	ex 415	. . . . . 6 ⊢ (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
54	53, 5	syl11 33	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
55	32, 54	pm2.61i 184	. . . 4 ⊢ (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
56	31, 55	jaoi 853	. . 3 ⊢ ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
57	3, 56	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58		prex 5335	. . 3 ⊢ {𝐴, 𝐵} ∈ V
59		eqeq1 2827	. . . 4 ⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60	59	2exbidv 1925	. . 3 ⊢ (𝑝 = {𝐴, 𝐵} → (∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
61	58, 60	elab 3669	. 2 ⊢ ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
62	57, 61	sylibr 236	1 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2801  Vcvv 3496  {csn 4569  {cpr 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-sn 4570  df-pr 4572

This theorem is referenced by: (None)