Metamath Proof Explorer

Theorem sprsymrelfvlem

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

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

Proof

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