Metamath Proof Explorer

Theorem frgr3vlem2

Description: Lemma 2 for frgr3v . (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Hypotheses frgr3v.v 
|- V = ( Vtx ` G )
frgr3v.e 
|- E = ( Edg ` G )
Assertion frgr3vlem2 
|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { C , A } e. E /\ { C , B } e. E ) ) ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v 
 |-  V = ( Vtx ` G )
2 frgr3v.e 
 |-  E = ( Edg ` G )
3 df-reu 
 |-  ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> E! x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) )
4 eleq1w 
 |-  ( x = y -> ( x e. { A , B , C } <-> y e. { A , B , C } ) )
5 preq1 
 |-  ( x = y -> { x , A } = { y , A } )
6 preq1 
 |-  ( x = y -> { x , B } = { y , B } )
7 5 6 preq12d 
 |-  ( x = y -> { { x , A } , { x , B } } = { { y , A } , { y , B } } )
8 7 sseq1d 
 |-  ( x = y -> ( { { x , A } , { x , B } } C_ E <-> { { y , A } , { y , B } } C_ E ) )
9 4 8 anbi12d 
 |-  ( x = y -> ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) <-> ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) )
10 9 eu4 
 |-  ( E! x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) <-> ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) ) )
11 1 2 frgr3vlem1 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) )
12 11 3expa 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) )
13 12 biantrud 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) <-> ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) ) ) )
14 vex 
 |-  x e. _V
15 14 eltp 
 |-  ( x e. { A , B , C } <-> ( x = A \/ x = B \/ x = C ) )
16 preq1 
 |-  ( x = A -> { x , A } = { A , A } )
17 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
18 16 17 preq12d 
 |-  ( x = A -> { { x , A } , { x , B } } = { { A , A } , { A , B } } )
19 18 sseq1d 
 |-  ( x = A -> ( { { x , A } , { x , B } } C_ E <-> { { A , A } , { A , B } } C_ E ) )
20 prex 
 |-  { A , A } e. _V
21 prex 
 |-  { A , B } e. _V
22 20 21 prss 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) <-> { { A , A } , { A , B } } C_ E )
23 2 usgredgne 
 |-  ( ( G e. USGraph /\ { A , A } e. E ) -> A =/= A )
24 23 adantll 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> A =/= A )
25 df-ne 
 |-  ( A =/= A <-> -. A = A )
26 eqid 
 |-  A = A
27 26 pm2.24i 
 |-  ( -. A = A -> ( { C , A } e. E /\ { C , B } e. E ) )
28 25 27 sylbi 
 |-  ( A =/= A -> ( { C , A } e. E /\ { C , B } e. E ) )
29 24 28 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { A , A } e. E ) -> ( { C , A } e. E /\ { C , B } e. E ) )
30 29 ex 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { A , A } e. E -> ( { C , A } e. E /\ { C , B } e. E ) ) )
31 30 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { A , A } e. E -> ( { C , A } e. E /\ { C , B } e. E ) ) )
32 31 com12 
 |-  ( { A , A } e. E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
33 32 adantr 
 |-  ( ( { A , A } e. E /\ { A , B } e. E ) -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
34 22 33 sylbir 
 |-  ( { { A , A } , { A , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
35 19 34 syl6bi 
 |-  ( x = A -> ( { { x , A } , { x , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
36 preq1 
 |-  ( x = B -> { x , A } = { B , A } )
37 preq1 
 |-  ( x = B -> { x , B } = { B , B } )
38 36 37 preq12d 
 |-  ( x = B -> { { x , A } , { x , B } } = { { B , A } , { B , B } } )
39 38 sseq1d 
 |-  ( x = B -> ( { { x , A } , { x , B } } C_ E <-> { { B , A } , { B , B } } C_ E ) )
40 prex 
 |-  { B , A } e. _V
41 prex 
 |-  { B , B } e. _V
42 40 41 prss 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) <-> { { B , A } , { B , B } } C_ E )
43 2 usgredgne 
 |-  ( ( G e. USGraph /\ { B , B } e. E ) -> B =/= B )
44 43 adantll 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> B =/= B )
45 df-ne 
 |-  ( B =/= B <-> -. B = B )
46 eqid 
 |-  B = B
47 46 pm2.24i 
 |-  ( -. B = B -> ( { C , A } e. E /\ { C , B } e. E ) )
48 45 47 sylbi 
 |-  ( B =/= B -> ( { C , A } e. E /\ { C , B } e. E ) )
49 44 48 syl 
 |-  ( ( ( V = { A , B , C } /\ G e. USGraph ) /\ { B , B } e. E ) -> ( { C , A } e. E /\ { C , B } e. E ) )
50 49 ex 
 |-  ( ( V = { A , B , C } /\ G e. USGraph ) -> ( { B , B } e. E -> ( { C , A } e. E /\ { C , B } e. E ) ) )
51 50 adantl 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { B , B } e. E -> ( { C , A } e. E /\ { C , B } e. E ) ) )
52 51 com12 
 |-  ( { B , B } e. E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
53 52 adantl 
 |-  ( ( { B , A } e. E /\ { B , B } e. E ) -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
54 42 53 sylbir 
 |-  ( { { B , A } , { B , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
55 39 54 syl6bi 
 |-  ( x = B -> ( { { x , A } , { x , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
56 preq1 
 |-  ( x = C -> { x , A } = { C , A } )
57 preq1 
 |-  ( x = C -> { x , B } = { C , B } )
58 56 57 preq12d 
 |-  ( x = C -> { { x , A } , { x , B } } = { { C , A } , { C , B } } )
59 58 sseq1d 
 |-  ( x = C -> ( { { x , A } , { x , B } } C_ E <-> { { C , A } , { C , B } } C_ E ) )
60 prex 
 |-  { C , A } e. _V
61 prex 
 |-  { C , B } e. _V
62 60 61 prss 
 |-  ( ( { C , A } e. E /\ { C , B } e. E ) <-> { { C , A } , { C , B } } C_ E )
63 ax-1 
 |-  ( ( { C , A } e. E /\ { C , B } e. E ) -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
64 62 63 sylbir 
 |-  ( { { C , A } , { C , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
65 59 64 syl6bi 
 |-  ( x = C -> ( { { x , A } , { x , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
66 35 55 65 3jaoi 
 |-  ( ( x = A \/ x = B \/ x = C ) -> ( { { x , A } , { x , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
67 15 66 sylbi 
 |-  ( x e. { A , B , C } -> ( { { x , A } , { x , B } } C_ E -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) ) )
68 67 imp 
 |-  ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) -> ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
69 68 com12 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
70 69 exlimdv 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) -> ( { C , A } e. E /\ { C , B } e. E ) ) )
71 prssi 
 |-  ( ( { C , A } e. E /\ { C , B } e. E ) -> { { C , A } , { C , B } } C_ E )
72 71 adantl 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) -> { { C , A } , { C , B } } C_ E )
73 72 3mix3d 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) -> ( { { A , A } , { A , B } } C_ E \/ { { B , A } , { B , B } } C_ E \/ { { C , A } , { C , B } } C_ E ) )
74 19 39 59 rextpg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( E. x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { { A , A } , { A , B } } C_ E \/ { { B , A } , { B , B } } C_ E \/ { { C , A } , { C , B } } C_ E ) ) )
75 74 ad3antrrr 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) -> ( E. x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { { A , A } , { A , B } } C_ E \/ { { B , A } , { B , B } } C_ E \/ { { C , A } , { C , B } } C_ E ) ) )
76 73 75 mpbird 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) -> E. x e. { A , B , C } { { x , A } , { x , B } } C_ E )
77 df-rex 
 |-  ( E. x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) )
78 76 77 sylib 
 |-  ( ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) /\ ( { C , A } e. E /\ { C , B } e. E ) ) -> E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) )
79 78 ex 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( { C , A } e. E /\ { C , B } e. E ) -> E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) ) )
80 70 79 impbid 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
81 13 80 bitr3d 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( ( E. x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ A. x A. y ( ( ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) /\ ( y e. { A , B , C } /\ { { y , A } , { y , B } } C_ E ) ) -> x = y ) ) <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
82 10 81 syl5bb 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x ( x e. { A , B , C } /\ { { x , A } , { x , B } } C_ E ) <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
83 3 82 syl5bb 
 |-  ( ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( V = { A , B , C } /\ G e. USGraph ) ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { C , A } e. E /\ { C , B } e. E ) ) )
84 83 ex 
 |-  ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( V = { A , B , C } /\ G e. USGraph ) -> ( E! x e. { A , B , C } { { x , A } , { x , B } } C_ E <-> ( { C , A } e. E /\ { C , B } e. E ) ) ) )