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 ∈ V ∨ B ∈ W → A B ∈ p | ∃ a ∃ b p = a b

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ V → A ∈ V
2 elex ⊢ B ∈ W → B ∈ V
3 1 2 orim12i ⊢ A ∈ V ∨ B ∈ W → A ∈ V ∨ B ∈ V
4 elisset ⊢ A ∈ V → ∃ a a = A
5 elisset ⊢ B ∈ V → ∃ b b = B
6 exdistrv ⊢ ∃ a ∃ b a = A ∧ b = B ↔ ∃ a a = A ∧ ∃ 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 ⊢ ∃ a ∃ b a = A ∧ b = B → ∃ a ∃ b A B = a b
10 6 9 sylbir ⊢ ∃ a a = A ∧ ∃ b b = B → ∃ a ∃ b A B = a b
11 4 5 10 syl2an ⊢ A ∈ V ∧ B ∈ V → ∃ a ∃ b A B = a b
12 11 expcom ⊢ B ∈ V → A ∈ V → ∃ a ∃ 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 → ∃ b A = a b
22 21 adantl ⊢ ¬ B ∈ V ∧ a = A → ∃ b A = a b
23 prprc2 ⊢ ¬ B ∈ V → A B = A
24 23 adantr ⊢ ¬ B ∈ V ∧ a = A → A B = A
25 24 eqeq1d ⊢ ¬ B ∈ V ∧ a = A → A B = a b ↔ A = a b
26 25 exbidv ⊢ ¬ B ∈ V ∧ a = A → ∃ b A B = a b ↔ ∃ b A = a b
27 22 26 mpbird ⊢ ¬ B ∈ V ∧ a = A → ∃ b A B = a b
28 27 ex ⊢ ¬ B ∈ V → a = A → ∃ b A B = a b
29 28 eximdv ⊢ ¬ B ∈ V → ∃ a a = A → ∃ a ∃ b A B = a b
30 4 29 syl5 ⊢ ¬ B ∈ V → A ∈ V → ∃ a ∃ b A B = a b
31 12 30 pm2.61i ⊢ A ∈ V → ∃ a ∃ b A B = a b
32 11 ex ⊢ A ∈ V → B ∈ V → ∃ a ∃ 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 → ∃ a B = a b
42 41 adantl ⊢ ¬ A ∈ V ∧ b = B → ∃ a B = a b
43 prprc1 ⊢ ¬ A ∈ V → A B = B
44 43 adantr ⊢ ¬ A ∈ V ∧ b = B → A B = B
45 44 eqeq1d ⊢ ¬ A ∈ V ∧ b = B → A B = a b ↔ B = a b
46 45 exbidv ⊢ ¬ A ∈ V ∧ b = B → ∃ a A B = a b ↔ ∃ a B = a b
47 42 46 mpbird ⊢ ¬ A ∈ V ∧ b = B → ∃ a A B = a b
48 47 ex ⊢ ¬ A ∈ V → b = B → ∃ a A B = a b
49 48 eximdv ⊢ ¬ A ∈ V → ∃ b b = B → ∃ b ∃ a A B = a b
50 49 impcom ⊢ ∃ b b = B ∧ ¬ A ∈ V → ∃ b ∃ a A B = a b
51 excom ⊢ ∃ a ∃ b A B = a b ↔ ∃ b ∃ a A B = a b
52 50 51 sylibr ⊢ ∃ b b = B ∧ ¬ A ∈ V → ∃ a ∃ b A B = a b
53 52 ex ⊢ ∃ b b = B → ¬ A ∈ V → ∃ a ∃ b A B = a b
54 53 5 syl11 ⊢ ¬ A ∈ V → B ∈ V → ∃ a ∃ b A B = a b
55 32 54 pm2.61i ⊢ B ∈ V → ∃ a ∃ b A B = a b
56 31 55 jaoi ⊢ A ∈ V ∨ B ∈ V → ∃ a ∃ b A B = a b
57 3 56 syl ⊢ A ∈ V ∨ B ∈ W → ∃ a ∃ b A B = a b
58 prex ⊢ A B ∈ V
59 eqeq1 ⊢ p = A B → p = a b ↔ A B = a b
60 59 2exbidv ⊢ p = A B → ∃ a ∃ b p = a b ↔ ∃ a ∃ b A B = a b
61 58 60 elab ⊢ A B ∈ p | ∃ a ∃ b p = a b ↔ ∃ a ∃ b A B = a b
62 57 61 sylibr ⊢ A ∈ V ∨ B ∈ W → A B ∈ p | ∃ a ∃ b p = a b