Metamath Proof Explorer

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 
|- ( ( A e. V \/ B e. W ) -> { A , B } e. { p | E. a E. b p = { a , b } } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 elex 
 |-  ( B e. W -> B e. _V )
3 1 2 orim12i 
 |-  ( ( A e. V \/ B e. W ) -> ( A e. _V \/ B e. _V ) )
4 elisset 
 |-  ( A e. _V -> E. a a = A )
5 elisset 
 |-  ( B e. _V -> E. b b = B )
6 exdistrv 
 |-  ( E. a E. b ( a = A /\ b = B ) <-> ( E. a a = A /\ E. b b = B ) )
7 preq12 
 |-  ( ( a = A /\ b = B ) -> { a , b } = { A , B } )
8 7 eqcomd 
 |-  ( ( a = A /\ b = B ) -> { A , B } = { a , b } )
9 8 2eximi 
 |-  ( E. a E. b ( a = A /\ b = B ) -> E. a E. b { A , B } = { a , b } )
10 6 9 sylbir 
 |-  ( ( E. a a = A /\ E. b b = B ) -> E. a E. b { A , B } = { a , b } )
11 4 5 10 syl2an 
 |-  ( ( A e. _V /\ B e. _V ) -> E. a E. b { A , B } = { a , b } )
12 11 expcom 
 |-  ( B e. _V -> ( A e. _V -> E. a E. b { A , B } = { a , b } ) )
13 preq2 
 |-  ( b = a -> { a , b } = { a , a } )
14 13 adantr 
 |-  ( ( b = a /\ a = A ) -> { a , b } = { a , a } )
15 dfsn2 
 |-  { a } = { a , a }
16 sneq 
 |-  ( a = A -> { a } = { A } )
17 16 adantl 
 |-  ( ( b = a /\ a = A ) -> { a } = { A } )
18 15 17 eqtr3id 
 |-  ( ( b = a /\ a = A ) -> { a , a } = { A } )
19 14 18 eqtr2d 
 |-  ( ( b = a /\ a = A ) -> { A } = { a , b } )
20 19 ex 
 |-  ( b = a -> ( a = A -> { A } = { a , b } ) )
21 20 spimevw 
 |-  ( a = A -> E. b { A } = { a , b } )
22 21 adantl 
 |-  ( ( -. B e. _V /\ a = A ) -> E. b { A } = { a , b } )
23 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
24 23 adantr 
 |-  ( ( -. B e. _V /\ a = A ) -> { A , B } = { A } )
25 24 eqeq1d 
 |-  ( ( -. B e. _V /\ a = A ) -> ( { A , B } = { a , b } <-> { A } = { a , b } ) )
26 25 exbidv 
 |-  ( ( -. B e. _V /\ a = A ) -> ( E. b { A , B } = { a , b } <-> E. b { A } = { a , b } ) )
27 22 26 mpbird 
 |-  ( ( -. B e. _V /\ a = A ) -> E. b { A , B } = { a , b } )
28 27 ex 
 |-  ( -. B e. _V -> ( a = A -> E. b { A , B } = { a , b } ) )
29 28 eximdv 
 |-  ( -. B e. _V -> ( E. a a = A -> E. a E. b { A , B } = { a , b } ) )
30 4 29 syl5 
 |-  ( -. B e. _V -> ( A e. _V -> E. a E. b { A , B } = { a , b } ) )
31 12 30 pm2.61i 
 |-  ( A e. _V -> E. a E. b { A , B } = { a , b } )
32 11 ex 
 |-  ( A e. _V -> ( B e. _V -> E. a E. b { A , B } = { a , b } ) )
33 preq1 
 |-  ( a = b -> { a , b } = { b , b } )
34 33 adantr 
 |-  ( ( a = b /\ b = B ) -> { a , b } = { b , b } )
35 dfsn2 
 |-  { b } = { b , b }
36 sneq 
 |-  ( b = B -> { b } = { B } )
37 36 adantl 
 |-  ( ( a = b /\ b = B ) -> { b } = { B } )
38 35 37 eqtr3id 
 |-  ( ( a = b /\ b = B ) -> { b , b } = { B } )
39 34 38 eqtr2d 
 |-  ( ( a = b /\ b = B ) -> { B } = { a , b } )
40 39 ex 
 |-  ( a = b -> ( b = B -> { B } = { a , b } ) )
41 40 spimevw 
 |-  ( b = B -> E. a { B } = { a , b } )
42 41 adantl 
 |-  ( ( -. A e. _V /\ b = B ) -> E. a { B } = { a , b } )
43 prprc1 
 |-  ( -. A e. _V -> { A , B } = { B } )
44 43 adantr 
 |-  ( ( -. A e. _V /\ b = B ) -> { A , B } = { B } )
45 44 eqeq1d 
 |-  ( ( -. A e. _V /\ b = B ) -> ( { A , B } = { a , b } <-> { B } = { a , b } ) )
46 45 exbidv 
 |-  ( ( -. A e. _V /\ b = B ) -> ( E. a { A , B } = { a , b } <-> E. a { B } = { a , b } ) )
47 42 46 mpbird 
 |-  ( ( -. A e. _V /\ b = B ) -> E. a { A , B } = { a , b } )
48 47 ex 
 |-  ( -. A e. _V -> ( b = B -> E. a { A , B } = { a , b } ) )
49 48 eximdv 
 |-  ( -. A e. _V -> ( E. b b = B -> E. b E. a { A , B } = { a , b } ) )
50 49 impcom 
 |-  ( ( E. b b = B /\ -. A e. _V ) -> E. b E. a { A , B } = { a , b } )
51 excom 
 |-  ( E. a E. b { A , B } = { a , b } <-> E. b E. a { A , B } = { a , b } )
52 50 51 sylibr 
 |-  ( ( E. b b = B /\ -. A e. _V ) -> E. a E. b { A , B } = { a , b } )
53 52 ex 
 |-  ( E. b b = B -> ( -. A e. _V -> E. a E. b { A , B } = { a , b } ) )
54 53 5 syl11 
 |-  ( -. A e. _V -> ( B e. _V -> E. a E. b { A , B } = { a , b } ) )
55 32 54 pm2.61i 
 |-  ( B e. _V -> E. a E. b { A , B } = { a , b } )
56 31 55 jaoi 
 |-  ( ( A e. _V \/ B e. _V ) -> E. a E. b { A , B } = { a , b } )
57 3 56 syl 
 |-  ( ( A e. V \/ B e. W ) -> E. a E. b { A , B } = { a , b } )
58 prex 
 |-  { A , B } e. _V
59 eqeq1 
 |-  ( p = { A , B } -> ( p = { a , b } <-> { A , B } = { a , b } ) )
60 59 2exbidv 
 |-  ( p = { A , B } -> ( E. a E. b p = { a , b } <-> E. a E. b { A , B } = { a , b } ) )
61 58 60 elab 
 |-  ( { A , B } e. { p | E. a E. b p = { a , b } } <-> E. a E. b { A , B } = { a , b } )
62 57 61 sylibr 
 |-  ( ( A e. V \/ B e. W ) -> { A , B } e. { p | E. a E. b p = { a , b } } )