Metamath Proof Explorer

Theorem sprsymrelfvlem

Description: Lemma for sprsymrelf and sprsymrelfv . (Contributed by AV, 19-Nov-2021)

Ref Expression
Assertion sprsymrelfvlem ⊢ P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V

Proof

Step Hyp Ref Expression
1 simpl ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → V ∈ V
2 eleq1 ⊢ c = x y → c ∈ P ↔ x y ∈ P
3 prsssprel ⊢ P ⊆ Pairs ⁡ V ∧ x y ∈ P ∧ x ∈ V ∧ y ∈ V → x ∈ V ∧ y ∈ V
4 3 3exp ⊢ P ⊆ Pairs ⁡ V → x y ∈ P → x ∈ V ∧ y ∈ V → x ∈ V ∧ y ∈ V
5 4 com13 ⊢ x ∈ V ∧ y ∈ V → x y ∈ P → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
6 5 el2v ⊢ x y ∈ P → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
7 2 6 biimtrdi ⊢ c = x y → c ∈ P → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
8 7 com12 ⊢ c ∈ P → c = x y → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
9 8 rexlimiv ⊢ ∃ c ∈ P c = x y → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
10 9 com12 ⊢ P ⊆ Pairs ⁡ V → ∃ c ∈ P c = x y → x ∈ V ∧ y ∈ V
11 10 adantl ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → ∃ c ∈ P c = x y → x ∈ V ∧ y ∈ V
12 11 imp ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V ∧ ∃ c ∈ P c = x y → x ∈ V ∧ y ∈ V
13 12 simpld ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V ∧ ∃ c ∈ P c = x y → x ∈ V
14 12 simprd ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V ∧ ∃ c ∈ P c = x y → y ∈ V
15 1 1 13 14 opabex2 ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ V
16 elopab ⊢ p ∈ x y | ∃ c ∈ P c = x y ↔ ∃ x ∃ y p = x y ∧ ∃ c ∈ P c = x y
17 9 adantl ⊢ p = x y ∧ ∃ c ∈ P c = x y → P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
18 17 adantld ⊢ p = x y ∧ ∃ c ∈ P c = x y → V ∈ V ∧ P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
19 18 imp ⊢ p = x y ∧ ∃ c ∈ P c = x y ∧ V ∈ V ∧ P ⊆ Pairs ⁡ V → x ∈ V ∧ y ∈ V
20 eleq1 ⊢ p = x y → p ∈ V × V ↔ x y ∈ V × V
21 20 ad2antrr ⊢ p = x y ∧ ∃ c ∈ P c = x y ∧ V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V ↔ x y ∈ V × V
22 opelxp ⊢ x y ∈ V × V ↔ x ∈ V ∧ y ∈ V
23 21 22 bitrdi ⊢ p = x y ∧ ∃ c ∈ P c = x y ∧ V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V ↔ x ∈ V ∧ y ∈ V
24 19 23 mpbird ⊢ p = x y ∧ ∃ c ∈ P c = x y ∧ V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V
25 24 ex ⊢ p = x y ∧ ∃ c ∈ P c = x y → V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V
26 25 exlimivv ⊢ ∃ x ∃ y p = x y ∧ ∃ c ∈ P c = x y → V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V
27 16 26 sylbi ⊢ p ∈ x y | ∃ c ∈ P c = x y → V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ V × V
28 27 com12 ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → p ∈ x y | ∃ c ∈ P c = x y → p ∈ V × V
29 28 ssrdv ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ⊆ V × V
30 15 29 elpwd ⊢ V ∈ V ∧ P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V
31 30 ex ⊢ V ∈ V → P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V
32 fvprc ⊢ ¬ V ∈ V → Pairs ⁡ V = ∅
33 32 sseq2d ⊢ ¬ V ∈ V → P ⊆ Pairs ⁡ V ↔ P ⊆ ∅
34 ss0b ⊢ P ⊆ ∅ ↔ P = ∅
35 33 34 bitrdi ⊢ ¬ V ∈ V → P ⊆ Pairs ⁡ V ↔ P = ∅
36 rex0 ⊢ ¬ ∃ c ∈ ∅ c = x y
37 rexeq ⊢ P = ∅ → ∃ c ∈ P c = x y ↔ ∃ c ∈ ∅ c = x y
38 36 37 mtbiri ⊢ P = ∅ → ¬ ∃ c ∈ P c = x y
39 38 alrimivv ⊢ P = ∅ → ∀ x ∀ y ¬ ∃ c ∈ P c = x y
40 opab0 ⊢ x y | ∃ c ∈ P c = x y = ∅ ↔ ∀ x ∀ y ¬ ∃ c ∈ P c = x y
41 39 40 sylibr ⊢ P = ∅ → x y | ∃ c ∈ P c = x y = ∅
42 0elpw ⊢ ∅ ∈ 𝒫 V × V
43 41 42 eqeltrdi ⊢ P = ∅ → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V
44 35 43 biimtrdi ⊢ ¬ V ∈ V → P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V
45 31 44 pm2.61i ⊢ P ⊆ Pairs ⁡ V → x y | ∃ c ∈ P c = x y ∈ 𝒫 V × V