Metamath Proof Explorer


Theorem upgrex

Description: An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v V = Vtx G
isupgr.e E = iEdg G
Assertion upgrex G UPGraph E Fn A F A x V y V E F = x y

Proof

Step Hyp Ref Expression
1 isupgr.v V = Vtx G
2 isupgr.e E = iEdg G
3 1 2 upgrn0 G UPGraph E Fn A F A E F
4 n0 E F x x E F
5 3 4 sylib G UPGraph E Fn A F A x x E F
6 simp1 G UPGraph E Fn A F A G UPGraph
7 fndm E Fn A dom E = A
8 7 eqcomd E Fn A A = dom E
9 8 eleq2d E Fn A F A F dom E
10 9 biimpd E Fn A F A F dom E
11 10 a1i G UPGraph E Fn A F A F dom E
12 11 3imp G UPGraph E Fn A F A F dom E
13 1 2 upgrss G UPGraph F dom E E F V
14 6 12 13 syl2anc G UPGraph E Fn A F A E F V
15 14 sselda G UPGraph E Fn A F A x E F x V
16 15 adantr G UPGraph E Fn A F A x E F E F x = x V
17 simpr G UPGraph E Fn A F A x E F E F x = E F x =
18 ssdif0 E F x E F x =
19 17 18 sylibr G UPGraph E Fn A F A x E F E F x = E F x
20 simpr G UPGraph E Fn A F A x E F x E F
21 20 snssd G UPGraph E Fn A F A x E F x E F
22 21 adantr G UPGraph E Fn A F A x E F E F x = x E F
23 19 22 eqssd G UPGraph E Fn A F A x E F E F x = E F = x
24 preq2 y = x x y = x x
25 dfsn2 x = x x
26 24 25 eqtr4di y = x x y = x
27 26 rspceeqv x V E F = x y V E F = x y
28 16 23 27 syl2anc G UPGraph E Fn A F A x E F E F x = y V E F = x y
29 n0 E F x y y E F x
30 14 adantr G UPGraph E Fn A F A x E F y E F x E F V
31 simprr G UPGraph E Fn A F A x E F y E F x y E F x
32 31 eldifad G UPGraph E Fn A F A x E F y E F x y E F
33 30 32 sseldd G UPGraph E Fn A F A x E F y E F x y V
34 1 2 upgrfi G UPGraph E Fn A F A E F Fin
35 34 adantr G UPGraph E Fn A F A x E F y E F x E F Fin
36 simprl G UPGraph E Fn A F A x E F y E F x x E F
37 36 32 prssd G UPGraph E Fn A F A x E F y E F x x y E F
38 fvex E F V
39 ssdomg E F V x y E F x y E F
40 38 37 39 mpsyl G UPGraph E Fn A F A x E F y E F x x y E F
41 1 2 upgrle G UPGraph E Fn A F A E F 2
42 41 adantr G UPGraph E Fn A F A x E F y E F x E F 2
43 eldifsni y E F x y x
44 43 ad2antll G UPGraph E Fn A F A x E F y E F x y x
45 44 necomd G UPGraph E Fn A F A x E F y E F x x y
46 hashprg x V y V x y x y = 2
47 46 el2v x y x y = 2
48 45 47 sylib G UPGraph E Fn A F A x E F y E F x x y = 2
49 42 48 breqtrrd G UPGraph E Fn A F A x E F y E F x E F x y
50 prfi x y Fin
51 hashdom E F Fin x y Fin E F x y E F x y
52 35 50 51 sylancl G UPGraph E Fn A F A x E F y E F x E F x y E F x y
53 49 52 mpbid G UPGraph E Fn A F A x E F y E F x E F x y
54 sbth x y E F E F x y x y E F
55 40 53 54 syl2anc G UPGraph E Fn A F A x E F y E F x x y E F
56 fisseneq E F Fin x y E F x y E F x y = E F
57 35 37 55 56 syl3anc G UPGraph E Fn A F A x E F y E F x x y = E F
58 57 eqcomd G UPGraph E Fn A F A x E F y E F x E F = x y
59 33 58 jca G UPGraph E Fn A F A x E F y E F x y V E F = x y
60 59 expr G UPGraph E Fn A F A x E F y E F x y V E F = x y
61 60 eximdv G UPGraph E Fn A F A x E F y y E F x y y V E F = x y
62 61 imp G UPGraph E Fn A F A x E F y y E F x y y V E F = x y
63 df-rex y V E F = x y y y V E F = x y
64 62 63 sylibr G UPGraph E Fn A F A x E F y y E F x y V E F = x y
65 29 64 sylan2b G UPGraph E Fn A F A x E F E F x y V E F = x y
66 28 65 pm2.61dane G UPGraph E Fn A F A x E F y V E F = x y
67 15 66 jca G UPGraph E Fn A F A x E F x V y V E F = x y
68 67 ex G UPGraph E Fn A F A x E F x V y V E F = x y
69 68 eximdv G UPGraph E Fn A F A x x E F x x V y V E F = x y
70 5 69 mpd G UPGraph E Fn A F A x x V y V E F = x y
71 df-rex x V y V E F = x y x x V y V E F = x y
72 70 71 sylibr G UPGraph E Fn A F A x V y V E F = x y