Theorem elsprel

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

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

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
3	1 2	orim12i	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) )
4		elisset	⊢ ( 𝐴 ∈ V → ∃ 𝑎 𝑎 = 𝐴 )
5		elisset	⊢ ( 𝐵 ∈ V → ∃ 𝑏 𝑏 = 𝐵 )
6		exdistrv	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ↔ ( ∃ 𝑎 𝑎 = 𝐴 ∧ ∃ 𝑏 𝑏 = 𝐵 ) )
7		preq12	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
8	7	eqcomd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
9	8	2eximi	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
10	6 9	sylbir	⊢ ( ( ∃ 𝑎 𝑎 = 𝐴 ∧ ∃ 𝑏 𝑏 = 𝐵 ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
11	4 5 10	syl2an	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
12	11	expcom	⊢ ( 𝐵 ∈ V → ( 𝐴 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
13		preq2	⊢ ( 𝑏 = 𝑎 → { 𝑎 , 𝑏 } = { 𝑎 , 𝑎 } )
14	13	adantr	⊢ ( ( 𝑏 = 𝑎 ∧ 𝑎 = 𝐴 ) → { 𝑎 , 𝑏 } = { 𝑎 , 𝑎 } )
15		dfsn2	⊢ { 𝑎 } = { 𝑎 , 𝑎 }
16		sneq	⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
17	16	adantl	⊢ ( ( 𝑏 = 𝑎 ∧ 𝑎 = 𝐴 ) → { 𝑎 } = { 𝐴 } )
18	15 17	eqtr3id	⊢ ( ( 𝑏 = 𝑎 ∧ 𝑎 = 𝐴 ) → { 𝑎 , 𝑎 } = { 𝐴 } )
19	14 18	eqtr2d	⊢ ( ( 𝑏 = 𝑎 ∧ 𝑎 = 𝐴 ) → { 𝐴 } = { 𝑎 , 𝑏 } )
20	19	ex	⊢ ( 𝑏 = 𝑎 → ( 𝑎 = 𝐴 → { 𝐴 } = { 𝑎 , 𝑏 } ) )
21	20	spimevw	⊢ ( 𝑎 = 𝐴 → ∃ 𝑏 { 𝐴 } = { 𝑎 , 𝑏 } )
22	21	adantl	⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴 ) → ∃ 𝑏 { 𝐴 } = { 𝑎 , 𝑏 } )
23		prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
24	23	adantr	⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴 ) → { 𝐴 , 𝐵 } = { 𝐴 } )
25	24	eqeq1d	⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ { 𝐴 } = { 𝑎 , 𝑏 } ) )
26	25	exbidv	⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴 ) → ( ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ∃ 𝑏 { 𝐴 } = { 𝑎 , 𝑏 } ) )
27	22 26	mpbird	⊢ ( ( ¬ 𝐵 ∈ V ∧ 𝑎 = 𝐴 ) → ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
28	27	ex	⊢ ( ¬ 𝐵 ∈ V → ( 𝑎 = 𝐴 → ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
29	28	eximdv	⊢ ( ¬ 𝐵 ∈ V → ( ∃ 𝑎 𝑎 = 𝐴 → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
30	4 29	syl5	⊢ ( ¬ 𝐵 ∈ V → ( 𝐴 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
31	12 30	pm2.61i	⊢ ( 𝐴 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
32	11	ex	⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
33		preq1	⊢ ( 𝑎 = 𝑏 → { 𝑎 , 𝑏 } = { 𝑏 , 𝑏 } )
34	33	adantr	⊢ ( ( 𝑎 = 𝑏 ∧ 𝑏 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝑏 , 𝑏 } )
35		dfsn2	⊢ { 𝑏 } = { 𝑏 , 𝑏 }
36		sneq	⊢ ( 𝑏 = 𝐵 → { 𝑏 } = { 𝐵 } )
37	36	adantl	⊢ ( ( 𝑎 = 𝑏 ∧ 𝑏 = 𝐵 ) → { 𝑏 } = { 𝐵 } )
38	35 37	eqtr3id	⊢ ( ( 𝑎 = 𝑏 ∧ 𝑏 = 𝐵 ) → { 𝑏 , 𝑏 } = { 𝐵 } )
39	34 38	eqtr2d	⊢ ( ( 𝑎 = 𝑏 ∧ 𝑏 = 𝐵 ) → { 𝐵 } = { 𝑎 , 𝑏 } )
40	39	ex	⊢ ( 𝑎 = 𝑏 → ( 𝑏 = 𝐵 → { 𝐵 } = { 𝑎 , 𝑏 } ) )
41	40	spimevw	⊢ ( 𝑏 = 𝐵 → ∃ 𝑎 { 𝐵 } = { 𝑎 , 𝑏 } )
42	41	adantl	⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵 ) → ∃ 𝑎 { 𝐵 } = { 𝑎 , 𝑏 } )
43		prprc1	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )
44	43	adantr	⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐵 } )
45	44	eqeq1d	⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ { 𝐵 } = { 𝑎 , 𝑏 } ) )
46	45	exbidv	⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵 ) → ( ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 { 𝐵 } = { 𝑎 , 𝑏 } ) )
47	42 46	mpbird	⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝑏 = 𝐵 ) → ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
48	47	ex	⊢ ( ¬ 𝐴 ∈ V → ( 𝑏 = 𝐵 → ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
49	48	eximdv	⊢ ( ¬ 𝐴 ∈ V → ( ∃ 𝑏 𝑏 = 𝐵 → ∃ 𝑏 ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
50	49	impcom	⊢ ( ( ∃ 𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑏 ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
51		excom	⊢ ( ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ↔ ∃ 𝑏 ∃ 𝑎 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
52	50 51	sylibr	⊢ ( ( ∃ 𝑏 𝑏 = 𝐵 ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
53	52	ex	⊢ ( ∃ 𝑏 𝑏 = 𝐵 → ( ¬ 𝐴 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
54	53 5	syl11	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
55	32 54	pm2.61i	⊢ ( 𝐵 ∈ V → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
56	31 55	jaoi	⊢ ( ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
57	3 56	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
58		prex	⊢ { 𝐴 , 𝐵 } ∈ V
59		eqeq1	⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( 𝑝 = { 𝑎 , 𝑏 } ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
60	59	2exbidv	⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
61	58 60	elab	⊢ ( { 𝐴 , 𝐵 } ∈ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } ↔ ∃ 𝑎 ∃ 𝑏 { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
62	57 61	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → { 𝐴 , 𝐵 } ∈ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )