Metamath Proof Explorer

Theorem 3vfriswmgrlem

Description: Lemma for 3vfriswmgr . (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v 
|- V = ( Vtx ` G )
3vfriswmgr.e 
|- E = ( Edg ` G )
Assertion 3vfriswmgrlem 
|- ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { A , B } e. E -> E! w e. { A , B } { A , w } e. E ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v 
 |-  V = ( Vtx ` G )
2 3vfriswmgr.e 
 |-  E = ( Edg ` G )
3 animorr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> ( { A , A } e. E \/ { A , B } e. E ) )
4 preq2 
 |-  ( w = A -> { A , w } = { A , A } )
5 4 eleq1d 
 |-  ( w = A -> ( { A , w } e. E <-> { A , A } e. E ) )
6 preq2 
 |-  ( w = B -> { A , w } = { A , B } )
7 6 eleq1d 
 |-  ( w = B -> ( { A , w } e. E <-> { A , B } e. E ) )
8 5 7 rexprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( E. w e. { A , B } { A , w } e. E <-> ( { A , A } e. E \/ { A , B } e. E ) ) )
9 8 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( E. w e. { A , B } { A , w } e. E <-> ( { A , A } e. E \/ { A , B } e. E ) ) )
10 9 ad2antrr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> ( E. w e. { A , B } { A , w } e. E <-> ( { A , A } e. E \/ { A , B } e. E ) ) )
11 3 10 mpbird 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> E. w e. { A , B } { A , w } e. E )
12 df-rex 
 |-  ( E. w e. { A , B } { A , w } e. E <-> E. w ( w e. { A , B } /\ { A , w } e. E ) )
13 11 12 sylib 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> E. w ( w e. { A , B } /\ { A , w } e. E ) )
14 vex 
 |-  w e. _V
15 14 elpr 
 |-  ( w e. { A , B } <-> ( w = A \/ w = B ) )
16 vex 
 |-  y e. _V
17 16 elpr 
 |-  ( y e. { A , B } <-> ( y = A \/ y = B ) )
18 eqidd 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = A )
19 18 a1i 
 |-  ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = A ) )
20 19 a1i13 
 |-  ( y = A -> ( { A , A } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = A ) ) ) )
21 preq2 
 |-  ( y = A -> { A , y } = { A , A } )
22 21 eleq1d 
 |-  ( y = A -> ( { A , y } e. E <-> { A , A } e. E ) )
23 eqeq2 
 |-  ( y = A -> ( A = y <-> A = A ) )
24 23 imbi2d 
 |-  ( y = A -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = A ) ) )
25 24 imbi2d 
 |-  ( y = A -> ( ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) <-> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = A ) ) ) )
26 20 22 25 3imtr4d 
 |-  ( y = A -> ( { A , y } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) ) )
27 2 usgredgne 
 |-  ( ( G e. USGraph /\ { A , A } e. E ) -> A =/= A )
28 27 adantll 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A =/= A )
29 df-ne 
 |-  ( A =/= A <-> -. A = A )
30 eqid 
 |-  A = A
31 30 pm2.24i 
 |-  ( -. A = A -> A = B )
32 29 31 sylbi 
 |-  ( A =/= A -> A = B )
33 28 32 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A = B )
34 33 ex 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { A , A } e. E -> A = B ) )
35 34 ad2antlr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> ( { A , A } e. E -> A = B ) )
36 35 com12 
 |-  ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = B ) )
37 36 2a1i 
 |-  ( y = B -> ( { A , B } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = B ) ) ) )
38 preq2 
 |-  ( y = B -> { A , y } = { A , B } )
39 38 eleq1d 
 |-  ( y = B -> ( { A , y } e. E <-> { A , B } e. E ) )
40 eqeq2 
 |-  ( y = B -> ( A = y <-> A = B ) )
41 40 imbi2d 
 |-  ( y = B -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = B ) ) )
42 41 imbi2d 
 |-  ( y = B -> ( ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) <-> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = B ) ) ) )
43 37 39 42 3imtr4d 
 |-  ( y = B -> ( { A , y } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) ) )
44 26 43 jaoi 
 |-  ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) ) )
45 eqeq1 
 |-  ( w = A -> ( w = y <-> A = y ) )
46 45 imbi2d 
 |-  ( w = A -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) )
47 5 46 imbi12d 
 |-  ( w = A -> ( ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) <-> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) ) )
48 47 imbi2d 
 |-  ( w = A -> ( ( { A , y } e. E -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) <-> ( { A , y } e. E -> ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A = y ) ) ) ) )
49 44 48 imbitrrid 
 |-  ( w = A -> ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) ) )
50 30 pm2.24i 
 |-  ( -. A = A -> B = A )
51 29 50 sylbi 
 |-  ( A =/= A -> B = A )
52 28 51 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> B = A )
53 52 ex 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { A , A } e. E -> B = A ) )
54 53 ad2antlr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> ( { A , A } e. E -> B = A ) )
55 54 com12 
 |-  ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = A ) )
56 55 a1i13 
 |-  ( y = A -> ( { A , A } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = A ) ) ) )
57 eqeq2 
 |-  ( y = A -> ( B = y <-> B = A ) )
58 57 imbi2d 
 |-  ( y = A -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = A ) ) )
59 58 imbi2d 
 |-  ( y = A -> ( ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) <-> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = A ) ) ) )
60 56 22 59 3imtr4d 
 |-  ( y = A -> ( { A , y } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) ) )
61 eqidd 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = B )
62 61 a1i 
 |-  ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = B ) )
63 62 a1i13 
 |-  ( y = B -> ( { A , B } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = B ) ) ) )
64 eqeq2 
 |-  ( y = B -> ( B = y <-> B = B ) )
65 64 imbi2d 
 |-  ( y = B -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = B ) ) )
66 65 imbi2d 
 |-  ( y = B -> ( ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) <-> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = B ) ) ) )
67 63 39 66 3imtr4d 
 |-  ( y = B -> ( { A , y } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) ) )
68 60 67 jaoi 
 |-  ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) ) )
69 eqeq1 
 |-  ( w = B -> ( w = y <-> B = y ) )
70 69 imbi2d 
 |-  ( w = B -> ( ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) <-> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) )
71 7 70 imbi12d 
 |-  ( w = B -> ( ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) <-> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) ) )
72 71 imbi2d 
 |-  ( w = B -> ( ( { A , y } e. E -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) <-> ( { A , y } e. E -> ( { A , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> B = y ) ) ) ) )
73 68 72 imbitrrid 
 |-  ( w = B -> ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) ) )
74 49 73 jaoi 
 |-  ( ( w = A \/ w = B ) -> ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) ) )
75 74 com3l 
 |-  ( ( y = A \/ y = B ) -> ( { A , y } e. E -> ( ( w = A \/ w = B ) -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) ) )
76 17 75 sylbi 
 |-  ( y e. { A , B } -> ( { A , y } e. E -> ( ( w = A \/ w = B ) -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) ) )
77 76 imp 
 |-  ( ( y e. { A , B } /\ { A , y } e. E ) -> ( ( w = A \/ w = B ) -> ( { A , w } e. E -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) )
78 77 com3l 
 |-  ( ( w = A \/ w = B ) -> ( { A , w } e. E -> ( ( y e. { A , B } /\ { A , y } e. E ) -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) )
79 15 78 sylbi 
 |-  ( w e. { A , B } -> ( { A , w } e. E -> ( ( y e. { A , B } /\ { A , y } e. E ) -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) ) ) )
80 79 imp31 
 |-  ( ( ( w e. { A , B } /\ { A , w } e. E ) /\ ( y e. { A , B } /\ { A , y } e. E ) ) -> ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> w = y ) )
81 80 com12 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> ( ( ( w e. { A , B } /\ { A , w } e. E ) /\ ( y e. { A , B } /\ { A , y } e. E ) ) -> w = y ) )
82 81 alrimivv 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> A. w A. y ( ( ( w e. { A , B } /\ { A , w } e. E ) /\ ( y e. { A , B } /\ { A , y } e. E ) ) -> w = y ) )
83 eleq1w 
 |-  ( w = y -> ( w e. { A , B } <-> y e. { A , B } ) )
84 preq2 
 |-  ( w = y -> { A , w } = { A , y } )
85 84 eleq1d 
 |-  ( w = y -> ( { A , w } e. E <-> { A , y } e. E ) )
86 83 85 anbi12d 
 |-  ( w = y -> ( ( w e. { A , B } /\ { A , w } e. E ) <-> ( y e. { A , B } /\ { A , y } e. E ) ) )
87 86 eu4 
 |-  ( E! w ( w e. { A , B } /\ { A , w } e. E ) <-> ( E. w ( w e. { A , B } /\ { A , w } e. E ) /\ A. w A. y ( ( ( w e. { A , B } /\ { A , w } e. E ) /\ ( y e. { A , B } /\ { A , y } e. E ) ) -> w = y ) ) )
88 13 82 87 sylanbrc 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> E! w ( w e. { A , B } /\ { A , w } e. E ) )
89 df-reu 
 |-  ( E! w e. { A , B } { A , w } e. E <-> E! w ( w e. { A , B } /\ { A , w } e. E ) )
90 88 89 sylibr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ { A , B } e. E ) -> E! w e. { A , B } { A , w } e. E )
91 90 ex 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { A , B } e. E -> E! w e. { A , B } { A , w } e. E ) )