Metamath Proof Explorer

Theorem frgr3vlem1

Description: Lemma 1 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 frgr3vlem1 ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgr3v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 vex ⊢ 𝑥 ∈ V
4 3 eltp ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
5 vex ⊢ 𝑦 ∈ V
6 5 eltp ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) )
7 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐴 )
8 7 a1i ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐴 ) )
9 8 a1i13 ⊢ ( 𝑦 = 𝐴 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐴 ) ) ) )
10 preq1 ⊢ ( 𝑦 = 𝐴 → { 𝑦 , 𝐴 } = { 𝐴 , 𝐴 } )
11 preq1 ⊢ ( 𝑦 = 𝐴 → { 𝑦 , 𝐵 } = { 𝐴 , 𝐵 } )
12 10 11 preq12d ⊢ ( 𝑦 = 𝐴 → { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } = { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } )
13 12 sseq1d ⊢ ( 𝑦 = 𝐴 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ) )
14 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐴 ) )
15 14 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐴 ) ) )
16 15 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐴 ) ) ) )
17 9 13 16 3imtr4d ⊢ ( 𝑦 = 𝐴 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) )
18 prex ⊢ { 𝐴 , 𝐴 } ∈ V
19 prex ⊢ { 𝐴 , 𝐵 } ∈ V
20 18 19 prss ⊢ ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 )
21 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 ≠ 𝐴 )
22 21 adantll ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 ≠ 𝐴 )
23 df-ne ⊢ ( 𝐴 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐴 )
24 eqid ⊢ 𝐴 = 𝐴
25 24 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → 𝐴 = 𝐵 )
26 23 25 sylbi ⊢ ( 𝐴 ≠ 𝐴 → 𝐴 = 𝐵 )
27 22 26 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 = 𝐵 )
28 27 expcom ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐵 ) )
29 28 adantr ⊢ ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐵 ) )
30 20 29 sylbir ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐵 ) )
31 30 com12 ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐴 = 𝐵 ) )
32 31 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐴 = 𝐵 ) )
33 32 com12 ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐵 ) )
34 33 2a1i ⊢ ( 𝑦 = 𝐵 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐵 ) ) ) )
35 preq1 ⊢ ( 𝑦 = 𝐵 → { 𝑦 , 𝐴 } = { 𝐵 , 𝐴 } )
36 preq1 ⊢ ( 𝑦 = 𝐵 → { 𝑦 , 𝐵 } = { 𝐵 , 𝐵 } )
37 35 36 preq12d ⊢ ( 𝑦 = 𝐵 → { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } = { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } )
38 37 sseq1d ⊢ ( 𝑦 = 𝐵 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ) )
39 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐵 ) )
40 39 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐵 ) ) )
41 40 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐵 ) ) ) )
42 34 38 41 3imtr4d ⊢ ( 𝑦 = 𝐵 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) )
43 24 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → 𝐴 = 𝐶 )
44 23 43 sylbi ⊢ ( 𝐴 ≠ 𝐴 → 𝐴 = 𝐶 )
45 22 44 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐴 = 𝐶 )
46 45 expcom ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐶 ) )
47 46 adantr ⊢ ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐶 ) )
48 20 47 sylbir ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐴 = 𝐶 ) )
49 48 com12 ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐴 = 𝐶 ) )
50 49 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐴 = 𝐶 ) )
51 50 com12 ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐶 ) )
52 51 2a1i ⊢ ( 𝑦 = 𝐶 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐶 ) ) ) )
53 preq1 ⊢ ( 𝑦 = 𝐶 → { 𝑦 , 𝐴 } = { 𝐶 , 𝐴 } )
54 preq1 ⊢ ( 𝑦 = 𝐶 → { 𝑦 , 𝐵 } = { 𝐶 , 𝐵 } )
55 53 54 preq12d ⊢ ( 𝑦 = 𝐶 → { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } = { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } )
56 55 sseq1d ⊢ ( 𝑦 = 𝐶 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) )
57 eqeq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐶 ) )
58 57 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐶 ) ) )
59 58 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝐶 ) ) ) )
60 52 56 59 3imtr4d ⊢ ( 𝑦 = 𝐶 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) )
61 17 42 60 3jaoi ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) )
62 preq1 ⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝐴 } = { 𝐴 , 𝐴 } )
63 preq1 ⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝐵 } = { 𝐴 , 𝐵 } )
64 62 63 preq12d ⊢ ( 𝑥 = 𝐴 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } )
65 64 sseq1d ⊢ ( 𝑥 = 𝐴 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 ) )
66 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
67 66 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) )
68 65 67 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ↔ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) )
69 68 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ↔ ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 = 𝑦 ) ) ) ) )
70 61 69 imbitrrid ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
71 prex ⊢ { 𝐵 , 𝐴 } ∈ V
72 prex ⊢ { 𝐵 , 𝐵 } ∈ V
73 71 72 prss ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) ↔ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 )
74 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵 ≠ 𝐵 )
75 74 adantll ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵 ≠ 𝐵 )
76 df-ne ⊢ ( 𝐵 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐵 )
77 eqid ⊢ 𝐵 = 𝐵
78 77 pm2.24i ⊢ ( ¬ 𝐵 = 𝐵 → 𝐵 = 𝐴 )
79 76 78 sylbi ⊢ ( 𝐵 ≠ 𝐵 → 𝐵 = 𝐴 )
80 75 79 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐴 )
81 80 expcom ⊢ ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐴 ) )
82 81 adantl ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐴 ) )
83 73 82 sylbir ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐴 ) )
84 83 com12 ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐵 = 𝐴 ) )
85 84 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐵 = 𝐴 ) )
86 85 com12 ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐴 ) )
87 86 2a1i ⊢ ( 𝑦 = 𝐴 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐴 ) ) ) )
88 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐴 ) )
89 88 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐴 ) ) )
90 89 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ↔ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐴 ) ) ) )
91 87 13 90 3imtr4d ⊢ ( 𝑦 = 𝐴 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) )
92 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐵 )
93 92 a1i ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐵 ) )
94 93 a1i13 ⊢ ( 𝑦 = 𝐵 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐵 ) ) ) )
95 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐵 ) )
96 95 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐵 ) ) )
97 96 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ↔ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐵 ) ) ) )
98 94 38 97 3imtr4d ⊢ ( 𝑦 = 𝐵 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) )
99 77 pm2.24i ⊢ ( ¬ 𝐵 = 𝐵 → 𝐵 = 𝐶 )
100 76 99 sylbi ⊢ ( 𝐵 ≠ 𝐵 → 𝐵 = 𝐶 )
101 75 100 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → 𝐵 = 𝐶 )
102 101 expcom ⊢ ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐶 ) )
103 102 adantl ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐶 ) )
104 73 103 sylbir ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐵 = 𝐶 ) )
105 104 com12 ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐵 = 𝐶 ) )
106 105 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐵 = 𝐶 ) )
107 106 com12 ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐶 ) )
108 107 2a1i ⊢ ( 𝑦 = 𝐶 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐶 ) ) ) )
109 eqeq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐶 ) )
110 109 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐶 ) ) )
111 110 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ↔ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝐶 ) ) ) )
112 108 56 111 3imtr4d ⊢ ( 𝑦 = 𝐶 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) )
113 91 98 112 3jaoi ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) )
114 preq1 ⊢ ( 𝑥 = 𝐵 → { 𝑥 , 𝐴 } = { 𝐵 , 𝐴 } )
115 preq1 ⊢ ( 𝑥 = 𝐵 → { 𝑥 , 𝐵 } = { 𝐵 , 𝐵 } )
116 114 115 preq12d ⊢ ( 𝑥 = 𝐵 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } )
117 116 sseq1d ⊢ ( 𝑥 = 𝐵 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 ) )
118 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝑦 ↔ 𝐵 = 𝑦 ) )
119 118 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) )
120 117 119 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ↔ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) )
121 120 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ↔ ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 = 𝑦 ) ) ) ) )
122 113 121 imbitrrid ⊢ ( 𝑥 = 𝐵 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
123 24 pm2.24i ⊢ ( ¬ 𝐴 = 𝐴 → 𝐶 = 𝐴 )
124 23 123 sylbi ⊢ ( 𝐴 ≠ 𝐴 → 𝐶 = 𝐴 )
125 22 124 syl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐴 , 𝐴 } ∈ 𝐸 ) → 𝐶 = 𝐴 )
126 125 expcom ⊢ ( { 𝐴 , 𝐴 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐶 = 𝐴 ) )
127 126 adantr ⊢ ( ( { 𝐴 , 𝐴 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐶 = 𝐴 ) )
128 20 127 sylbir ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝐶 = 𝐴 ) )
129 128 com12 ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐶 = 𝐴 ) )
130 129 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → 𝐶 = 𝐴 ) )
131 130 com12 ⊢ ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐴 ) )
132 131 a1i13 ⊢ ( 𝑦 = 𝐴 → ( { { 𝐴 , 𝐴 } , { 𝐴 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐴 ) ) ) )
133 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐶 = 𝑦 ↔ 𝐶 = 𝐴 ) )
134 133 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐴 ) ) )
135 134 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ↔ ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐴 ) ) ) )
136 132 13 135 3imtr4d ⊢ ( 𝑦 = 𝐴 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) )
137 pm2.21 ⊢ ( ¬ 𝐵 = 𝐵 → ( 𝐵 = 𝐵 → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) ) )
138 76 137 sylbi ⊢ ( 𝐵 ≠ 𝐵 → ( 𝐵 = 𝐵 → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) ) )
139 75 77 138 mpisyl ⊢ ( ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) )
140 139 expcom ⊢ ( { 𝐵 , 𝐵 } ∈ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) ) )
141 140 adantl ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐵 } ∈ 𝐸 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) ) )
142 73 141 sylbir ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 = 𝐵 ) ) )
143 142 com13 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐶 = 𝐵 ) ) )
144 143 a1d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐶 = 𝐵 ) ) ) )
145 144 3imp ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → 𝐶 = 𝐵 ) )
146 145 com12 ⊢ ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐵 ) )
147 146 a1i13 ⊢ ( 𝑦 = 𝐵 → ( { { 𝐵 , 𝐴 } , { 𝐵 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐵 ) ) ) )
148 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐶 = 𝑦 ↔ 𝐶 = 𝐵 ) )
149 148 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐵 ) ) )
150 149 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ↔ ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐵 ) ) ) )
151 147 38 150 3imtr4d ⊢ ( 𝑦 = 𝐵 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) )
152 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐶 )
153 152 a1i ⊢ ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐶 ) )
154 153 a1i13 ⊢ ( 𝑦 = 𝐶 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐶 ) ) ) )
155 eqeq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐶 = 𝑦 ↔ 𝐶 = 𝐶 ) )
156 155 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐶 ) ) )
157 156 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ↔ ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝐶 ) ) ) )
158 154 56 157 3imtr4d ⊢ ( 𝑦 = 𝐶 → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) )
159 136 151 158 3jaoi ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) )
160 preq1 ⊢ ( 𝑥 = 𝐶 → { 𝑥 , 𝐴 } = { 𝐶 , 𝐴 } )
161 preq1 ⊢ ( 𝑥 = 𝐶 → { 𝑥 , 𝐵 } = { 𝐶 , 𝐵 } )
162 160 161 preq12d ⊢ ( 𝑥 = 𝐶 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } = { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } )
163 162 sseq1d ⊢ ( 𝑥 = 𝐶 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 ) )
164 eqeq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 = 𝑦 ↔ 𝐶 = 𝑦 ) )
165 164 imbi2d ⊢ ( 𝑥 = 𝐶 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) )
166 163 165 imbi12d ⊢ ( 𝑥 = 𝐶 → ( ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ↔ ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) )
167 166 imbi2d ⊢ ( 𝑥 = 𝐶 → ( ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ↔ ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝐶 , 𝐴 } , { 𝐶 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 = 𝑦 ) ) ) ) )
168 159 167 imbitrrid ⊢ ( 𝑥 = 𝐶 → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
169 70 122 168 3jaoi ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
170 169 com3l ⊢ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ∨ 𝑦 = 𝐶 ) → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
171 6 170 sylbi ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) ) )
172 171 imp ⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) )
173 172 com3l ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) )
174 4 173 sylbi ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) ) ) )
175 174 imp31 ⊢ ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝑥 = 𝑦 ) )
176 175 com12 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) )
177 176 alrimivv ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ∧ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑦 , 𝐴 } , { 𝑦 , 𝐵 } } ⊆ 𝐸 ) ) → 𝑥 = 𝑦 ) )