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=VtxG
frgr3v.e E=EdgG
Assertion frgr3vlem2 AXBYCZABACBCV=ABCGUSGraph∃!xABCxAxBECAECBE

Proof

Step Hyp Ref Expression
1 frgr3v.v V=VtxG
2 frgr3v.e E=EdgG
3 df-reu ∃!xABCxAxBE∃!xxABCxAxBE
4 eleq1w x=yxABCyABC
5 preq1 x=yxA=yA
6 preq1 x=yxB=yB
7 5 6 preq12d x=yxAxB=yAyB
8 7 sseq1d x=yxAxBEyAyBE
9 4 8 anbi12d x=yxABCxAxBEyABCyAyBE
10 9 eu4 ∃!xxABCxAxBExxABCxAxBExyxABCxAxBEyABCyAyBEx=y
11 1 2 frgr3vlem1 AXBYCZABACBCV=ABCGUSGraphxyxABCxAxBEyABCyAyBEx=y
12 11 3expa AXBYCZABACBCV=ABCGUSGraphxyxABCxAxBEyABCyAyBEx=y
13 12 biantrud AXBYCZABACBCV=ABCGUSGraphxxABCxAxBExxABCxAxBExyxABCxAxBEyABCyAyBEx=y
14 vex xV
15 14 eltp xABCx=Ax=Bx=C
16 preq1 x=AxA=AA
17 preq1 x=AxB=AB
18 16 17 preq12d x=AxAxB=AAAB
19 18 sseq1d x=AxAxBEAAABE
20 prex AAV
21 prex ABV
22 20 21 prss AAEABEAAABE
23 2 usgredgne GUSGraphAAEAA
24 23 adantll V=ABCGUSGraphAAEAA
25 df-ne AA¬A=A
26 eqid A=A
27 26 pm2.24i ¬A=ACAECBE
28 25 27 sylbi AACAECBE
29 24 28 syl V=ABCGUSGraphAAECAECBE
30 29 ex V=ABCGUSGraphAAECAECBE
31 30 adantl AXBYCZABACBCV=ABCGUSGraphAAECAECBE
32 31 com12 AAEAXBYCZABACBCV=ABCGUSGraphCAECBE
33 32 adantr AAEABEAXBYCZABACBCV=ABCGUSGraphCAECBE
34 22 33 sylbir AAABEAXBYCZABACBCV=ABCGUSGraphCAECBE
35 19 34 syl6bi x=AxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
36 preq1 x=BxA=BA
37 preq1 x=BxB=BB
38 36 37 preq12d x=BxAxB=BABB
39 38 sseq1d x=BxAxBEBABBE
40 prex BAV
41 prex BBV
42 40 41 prss BAEBBEBABBE
43 2 usgredgne GUSGraphBBEBB
44 43 adantll V=ABCGUSGraphBBEBB
45 df-ne BB¬B=B
46 eqid B=B
47 46 pm2.24i ¬B=BCAECBE
48 45 47 sylbi BBCAECBE
49 44 48 syl V=ABCGUSGraphBBECAECBE
50 49 ex V=ABCGUSGraphBBECAECBE
51 50 adantl AXBYCZABACBCV=ABCGUSGraphBBECAECBE
52 51 com12 BBEAXBYCZABACBCV=ABCGUSGraphCAECBE
53 52 adantl BAEBBEAXBYCZABACBCV=ABCGUSGraphCAECBE
54 42 53 sylbir BABBEAXBYCZABACBCV=ABCGUSGraphCAECBE
55 39 54 syl6bi x=BxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
56 preq1 x=CxA=CA
57 preq1 x=CxB=CB
58 56 57 preq12d x=CxAxB=CACB
59 58 sseq1d x=CxAxBECACBE
60 prex CAV
61 prex CBV
62 60 61 prss CAECBECACBE
63 ax-1 CAECBEAXBYCZABACBCV=ABCGUSGraphCAECBE
64 62 63 sylbir CACBEAXBYCZABACBCV=ABCGUSGraphCAECBE
65 59 64 syl6bi x=CxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
66 35 55 65 3jaoi x=Ax=Bx=CxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
67 15 66 sylbi xABCxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
68 67 imp xABCxAxBEAXBYCZABACBCV=ABCGUSGraphCAECBE
69 68 com12 AXBYCZABACBCV=ABCGUSGraphxABCxAxBECAECBE
70 69 exlimdv AXBYCZABACBCV=ABCGUSGraphxxABCxAxBECAECBE
71 prssi CAECBECACBE
72 71 adantl AXBYCZABACBCV=ABCGUSGraphCAECBECACBE
73 72 3mix3d AXBYCZABACBCV=ABCGUSGraphCAECBEAAABEBABBECACBE
74 19 39 59 rextpg AXBYCZxABCxAxBEAAABEBABBECACBE
75 74 ad3antrrr AXBYCZABACBCV=ABCGUSGraphCAECBExABCxAxBEAAABEBABBECACBE
76 73 75 mpbird AXBYCZABACBCV=ABCGUSGraphCAECBExABCxAxBE
77 df-rex xABCxAxBExxABCxAxBE
78 76 77 sylib AXBYCZABACBCV=ABCGUSGraphCAECBExxABCxAxBE
79 78 ex AXBYCZABACBCV=ABCGUSGraphCAECBExxABCxAxBE
80 70 79 impbid AXBYCZABACBCV=ABCGUSGraphxxABCxAxBECAECBE
81 13 80 bitr3d AXBYCZABACBCV=ABCGUSGraphxxABCxAxBExyxABCxAxBEyABCyAyBEx=yCAECBE
82 10 81 syl5bb AXBYCZABACBCV=ABCGUSGraph∃!xxABCxAxBECAECBE
83 3 82 syl5bb AXBYCZABACBCV=ABCGUSGraph∃!xABCxAxBECAECBE
84 83 ex AXBYCZABACBCV=ABCGUSGraph∃!xABCxAxBECAECBE