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 syl6bi 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 syl6bi ¬ 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