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 biimtrdi ⊢ ( 𝑥 = 𝐴 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ 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 biimtrdi ⊢ ( 𝑥 = 𝐵 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ 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 biimtrdi ⊢ ( 𝑥 = 𝐶 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 → ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ 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 bitrid ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
83 3 82 bitrid ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
84 83 ex ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )