Theorem elsprel 41725

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 4302, which is not an element of all unordered pairs, see spr0nelg 41726. (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 3212	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3212	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3	1, 2	orim12i 538	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4		elisset 3215	. . . . . . 7 ⊢ (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5		elisset 3215	. . . . . . 7 ⊢ (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6		eeanv 2182	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7		preq12 4270	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
8	7	eqcomd 2628	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
9	8	2eximi 1763	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
10	6, 9	sylbir 225	. . . . . . 7 ⊢ ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
11	4, 5, 10	syl2an 494	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
12	11	expcom 451	. . . . 5 ⊢ (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13		preq2 4269	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
14	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15		dfsn2 4190	. . . . . . . . . . . . . 14 ⊢ {𝑎} = {𝑎, 𝑎}
16		sneq 4187	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
17	16	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎} = {𝐴})
18	15, 17	syl5eqr 2670	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
19	14, 18	eqtr2d 2657	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
20	19	ex 450	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
21	20	spimev 2259	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
22	21	adantl 482	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23		prprc2 4301	. . . . . . . . . . . 12 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
24	23	adantr 481	. . . . . . . . . . 11 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2624	. . . . . . . . . 10 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
26	25	exbidv 1850	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
27	22, 26	mpbird 247	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
28	27	ex 450	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
29	28	eximdv 1846	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
30	4, 29	syl5 34	. . . . 5 ⊢ (¬ 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
31	12, 30	pm2.61i 176	. . . 4 ⊢ (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
32	11	ex 450	. . . . 5 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33		preq1 4268	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
34	33	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35		dfsn2 4190	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} = {𝑏, 𝑏}
36		sneq 4187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
37	36	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏} = {𝐵})
38	35, 37	syl5eqr 2670	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
39	34, 38	eqtr2d 2657	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
40	39	ex 450	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
41	40	spimev 2259	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
42	41	adantl 482	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43		prprc1 4300	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
44	43	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
45	44	eqeq1d 2624	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
46	45	exbidv 1850	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
47	42, 46	mpbird 247	. . . . . . . . . . 11 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
48	47	ex 450	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
49	48	eximdv 1846	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
50	49	impcom 446	. . . . . . . 8 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51		excom 2042	. . . . . . . 8 ⊢ (∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
52	50, 51	sylibr 224	. . . . . . 7 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
53	52	ex 450	. . . . . 6 ⊢ (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
54	53, 5	syl11 33	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
55	32, 54	pm2.61i 176	. . . 4 ⊢ (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
56	31, 55	jaoi 394	. . 3 ⊢ ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
57	3, 56	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58		prex 4909	. . 3 ⊢ {𝐴, 𝐵} ∈ V
59		eqeq1 2626	. . . 4 ⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60	59	2exbidv 1852	. . 3 ⊢ (𝑝 = {𝐴, 𝐵} → (∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
61	58, 60	elab 3350	. 2 ⊢ ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
62	57, 61	sylibr 224	1 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  Vcvv 3200  {csn 4177  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180

This theorem is referenced by: (None)