Theorem elsprel 44927

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 4703, which is not an element of all unordered pairs, see spr0nelg 44928. (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 3450	. . . 4 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3450	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3	1, 2	orim12i 906	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ V ∨ 𝐵 ∈ V))
4		elisset 2820	. . . . . . 7 ⊢ (𝐴 ∈ V → ∃𝑎 𝑎 = 𝐴)
5		elisset 2820	. . . . . . 7 ⊢ (𝐵 ∈ V → ∃𝑏 𝑏 = 𝐵)
6		exdistrv 1959	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ↔ (∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵))
7		preq12 4671	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝐴, 𝐵})
8	7	eqcomd 2744	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝑎, 𝑏})
9	8	2eximi 1838	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
10	6, 9	sylbir 234	. . . . . . 7 ⊢ ((∃𝑎 𝑎 = 𝐴 ∧ ∃𝑏 𝑏 = 𝐵) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
11	4, 5, 10	syl2an 596	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
12	11	expcom 414	. . . . 5 ⊢ (𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
13		preq2 4670	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → {𝑎, 𝑏} = {𝑎, 𝑎})
14	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑏} = {𝑎, 𝑎})
15		dfsn2 4574	. . . . . . . . . . . . . 14 ⊢ {𝑎} = {𝑎, 𝑎}
16		sneq 4571	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
17	16	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎} = {𝐴})
18	15, 17	eqtr3id 2792	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝑎, 𝑎} = {𝐴})
19	14, 18	eqtr2d 2779	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 = 𝐴) → {𝐴} = {𝑎, 𝑏})
20	19	ex 413	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑎 → (𝑎 = 𝐴 → {𝐴} = {𝑎, 𝑏}))
21	20	spimevw 1998	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ∃𝑏{𝐴} = {𝑎, 𝑏})
22	21	adantl 482	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴} = {𝑎, 𝑏})
23		prprc2 4702	. . . . . . . . . . . 12 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
24	23	adantr 481	. . . . . . . . . . 11 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → {𝐴, 𝐵} = {𝐴})
25	24	eqeq1d 2740	. . . . . . . . . 10 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐴} = {𝑎, 𝑏}))
26	25	exbidv 1924	. . . . . . . . 9 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → (∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏{𝐴} = {𝑎, 𝑏}))
27	22, 26	mpbird 256	. . . . . . . 8 ⊢ ((¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴) → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
28	27	ex 413	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (𝑎 = 𝐴 → ∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
29	28	eximdv 1920	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → (∃𝑎 𝑎 = 𝐴 → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
30	4, 29	syl5 34	. . . . 5 ⊢ (¬ 𝐵 ∈ V → (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
31	12, 30	pm2.61i 182	. . . 4 ⊢ (𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
32	11	ex 413	. . . . 5 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
33		preq1 4669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → {𝑎, 𝑏} = {𝑏, 𝑏})
34	33	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑎, 𝑏} = {𝑏, 𝑏})
35		dfsn2 4574	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} = {𝑏, 𝑏}
36		sneq 4571	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
37	36	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏} = {𝐵})
38	35, 37	eqtr3id 2792	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝑏, 𝑏} = {𝐵})
39	34, 38	eqtr2d 2779	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑏 ∧ 𝑏 = 𝐵) → {𝐵} = {𝑎, 𝑏})
40	39	ex 413	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑏 = 𝐵 → {𝐵} = {𝑎, 𝑏}))
41	40	spimevw 1998	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ∃𝑎{𝐵} = {𝑎, 𝑏})
42	41	adantl 482	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐵} = {𝑎, 𝑏})
43		prprc1 4701	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
44	43	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → {𝐴, 𝐵} = {𝐵})
45	44	eqeq1d 2740	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ {𝐵} = {𝑎, 𝑏}))
46	45	exbidv 1924	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → (∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑎{𝐵} = {𝑎, 𝑏}))
47	42, 46	mpbird 256	. . . . . . . . . . 11 ⊢ ((¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵) → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
48	47	ex 413	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑏 = 𝐵 → ∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
49	48	eximdv 1920	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (∃𝑏 𝑏 = 𝐵 → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏}))
50	49	impcom 408	. . . . . . . 8 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
51		excom 2162	. . . . . . . 8 ⊢ (∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏} ↔ ∃𝑏∃𝑎{𝐴, 𝐵} = {𝑎, 𝑏})
52	50, 51	sylibr 233	. . . . . . 7 ⊢ ((∃𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
53	52	ex 413	. . . . . 6 ⊢ (∃𝑏 𝑏 = 𝐵 → (¬ 𝐴 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
54	53, 5	syl11 33	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
55	32, 54	pm2.61i 182	. . . 4 ⊢ (𝐵 ∈ V → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
56	31, 55	jaoi 854	. . 3 ⊢ ((𝐴 ∈ V ∨ 𝐵 ∈ V) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
57	3, 56	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
58		prex 5355	. . 3 ⊢ {𝐴, 𝐵} ∈ V
59		eqeq1 2742	. . . 4 ⊢ (𝑝 = {𝐴, 𝐵} → (𝑝 = {𝑎, 𝑏} ↔ {𝐴, 𝐵} = {𝑎, 𝑏}))
60	59	2exbidv 1927	. . 3 ⊢ (𝑝 = {𝐴, 𝐵} → (∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏}))
61	58, 60	elab 3609	. 2 ⊢ ({𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑎∃𝑏{𝐴, 𝐵} = {𝑎, 𝑏})
62	57, 61	sylibr 233	1 ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1539  ∃wex 1782   ∈ wcel 2106  {cab 2715  Vcvv 3432  {csn 4561  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-sn 4562  df-pr 4564

This theorem is referenced by: (None)