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 𝑉 = ( Vtx ‘ 𝐺 )
frgr3v.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgr3vlem2 ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v 𝑉 = ( Vtx ‘ 𝐺 )
2 frgr3v.e 𝐸 = ( Edg ‘ 𝐺 )
3 df-reu ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ∃! 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
4 eleq1w ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ) )
5 preq1 ( 𝑥 = 𝑦 → { 𝑥 , 𝐴 } = { 𝑦 , 𝐴 } )
6 preq1 ( 𝑥 = 𝑦 → { 𝑥 , 𝐵 } = { 𝑦 , 𝐵 } )
7 5 6 preq12d ( 𝑥 = 𝑦 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } )
8 7 sseq1d ( 𝑥 = 𝑦 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) )
9 4 8 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) )
10 9 eu4 ( ∃! 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ∀ 𝑥𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) ) )
11 1 2 frgr3vlem1 ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ∀ 𝑥𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) )
12 11 3expa ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ∀ 𝑥𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) )
13 12 biantrud ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ∀ 𝑥𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) ) ) )
14 vex 𝑥 ∈ V
15 14 eltp ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶 ) )
16 preq1 ( 𝑥 = 𝐴 → { 𝑥 , 𝐴 } = { 𝐴 , 𝐴 } )
17 preq1 ( 𝑥 = 𝐴 → { 𝑥 , 𝐵 } = { 𝐴 , 𝐵 } )
18 16 17 preq12d ( 𝑥 = 𝐴 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } )
19 18 sseq1d ( 𝑥 = 𝐴 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ) )
20 prex { 𝐴 , 𝐴 } ∈ V
21 prex { 𝐴 , 𝐵 } ∈ V
22 20 21 prss ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 )
23 2 usgredgne ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴𝐴 )
24 23 adantll ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴𝐴 )
25 df-ne ( 𝐴𝐴 ↔ ¬ 𝐴 = 𝐴 )
26 eqid 𝐴 = 𝐴
27 26 pm2.24i ( ¬ 𝐴 = 𝐴 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
28 25 27 sylbi ( 𝐴𝐴 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
29 24 28 syl ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
30 29 ex ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
31 30 adantl ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
32 31 com12 ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
33 32 adantr ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
34 22 33 sylbir ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
35 19 34 syl6bi ( 𝑥 = 𝐴 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
36 preq1 ( 𝑥 = 𝐵 → { 𝑥 , 𝐴 } = { 𝐵 , 𝐴 } )
37 preq1 ( 𝑥 = 𝐵 → { 𝑥 , 𝐵 } = { 𝐵 , 𝐵 } )
38 36 37 preq12d ( 𝑥 = 𝐵 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } )
39 38 sseq1d ( 𝑥 = 𝐵 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ) )
40 prex { 𝐵 , 𝐴 } ∈ V
41 prex { 𝐵 , 𝐵 } ∈ V
42 40 41 prss ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) ↔ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 )
43 2 usgredgne ( ( 𝐺 ∈ USGraph ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵𝐵 )
44 43 adantll ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵𝐵 )
45 df-ne ( 𝐵𝐵 ↔ ¬ 𝐵 = 𝐵 )
46 eqid 𝐵 = 𝐵
47 46 pm2.24i ( ¬ 𝐵 = 𝐵 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
48 45 47 sylbi ( 𝐵𝐵 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
49 44 48 syl ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
50 49 ex ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
51 50 adantl ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
52 51 com12 ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
53 52 adantl ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
54 42 53 sylbir ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
55 39 54 syl6bi ( 𝑥 = 𝐵 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
56 preq1 ( 𝑥 = 𝐶 → { 𝑥 , 𝐴 } = { 𝐶 , 𝐴 } )
57 preq1 ( 𝑥 = 𝐶 → { 𝑥 , 𝐵 } = { 𝐶 , 𝐵 } )
58 56 57 preq12d ( 𝑥 = 𝐶 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } )
59 58 sseq1d ( 𝑥 = 𝐶 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) )
60 prex { 𝐶 , 𝐴 } ∈ V
61 prex { 𝐶 , 𝐵 } ∈ V
62 60 61 prss ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 )
63 ax-1 ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
64 62 63 sylbir ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
65 59 64 syl6bi ( 𝑥 = 𝐶 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
66 35 55 65 3jaoi ( ( 𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶 ) → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
67 15 66 sylbi ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
68 67 imp ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) → ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
69 68 com12 ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
70 69 exlimdv ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) → ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
71 prssi ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) → { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 )
72 71 adantl ( ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) → { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 )
73 72 3mix3d ( ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) )
74 19 39 59 rextpg ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) ) )
75 74 ad3antrrr ( ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) → ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ∨ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) ) )
76 73 75 mpbird ( ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 )
77 df-rex ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
78 76 77 sylib ( ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) → ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
79 78 ex ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) → ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) )
80 70 79 impbid ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
81 13 80 bitr3d ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∃ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ∀ 𝑥𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) ) ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
82 10 81 syl5bb ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
83 3 82 syl5bb ( ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
84 83 ex ( ( ( 𝐴𝑋𝐵𝑌𝐶𝑍 ) ∧ ( 𝐴𝐵𝐴𝐶𝐵𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )