Metamath Proof Explorer

Theorem 3vfriswmgr

Description: Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 3vfriswmgr ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
4 1 2 frgr3v ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) )
5 4 exp4b ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐺 ∈ USGraph → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) ) ) )
6 5 3imp1 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
7 prcom ⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
8 7 eleq1i ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐶 } ∈ 𝐸 )
9 8 biimpi ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 → { 𝐴 , 𝐶 } ∈ 𝐸 )
10 9 3ad2ant3 ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → { 𝐴 , 𝐶 } ∈ 𝐸 )
11 10 adantl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → { 𝐴 , 𝐶 } ∈ 𝐸 )
12 simpl11 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → 𝐴 ∈ 𝑋 )
13 simpl12 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → 𝐵 ∈ 𝑌 )
14 simp1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝐴 ≠ 𝐵 )
15 14 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → 𝐴 ≠ 𝐵 )
16 15 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → 𝐴 ≠ 𝐵 )
17 12 13 16 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) )
18 simp3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
19 18 anim1i ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
20 17 19 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) )
21 simp1 ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → { 𝐴 , 𝐵 } ∈ 𝐸 )
22 1 2 3vfriswmgrlem ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) )
23 22 imp ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 )
24 20 21 23 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 )
25 11 24 jca ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) )
26 simpr2 ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → { 𝐵 , 𝐶 } ∈ 𝐸 )
27 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
28 27 biimpi ⊢ ( 𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴 )
29 28 3ad2ant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐴 )
30 29 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → 𝐵 ≠ 𝐴 )
31 30 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → 𝐵 ≠ 𝐴 )
32 13 12 31 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) )
33 tpcoma ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 , 𝐶 }
34 18 33 eqtrdi ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → 𝑉 = { 𝐵 , 𝐴 , 𝐶 } )
35 34 anim1i ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
36 32 35 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) )
37 prcom ⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
38 37 eleq1i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐵 , 𝐴 } ∈ 𝐸 )
39 38 biimpi ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → { 𝐵 , 𝐴 } ∈ 𝐸 )
40 39 3ad2ant1 ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → { 𝐵 , 𝐴 } ∈ 𝐸 )
41 1 2 3vfriswmgrlem ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( { 𝐵 , 𝐴 } ∈ 𝐸 → ∃! 𝑤 ∈ { 𝐵 , 𝐴 } { 𝐵 , 𝑤 } ∈ 𝐸 ) )
42 41 imp ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) → ∃! 𝑤 ∈ { 𝐵 , 𝐴 } { 𝐵 , 𝑤 } ∈ 𝐸 )
43 reueq1 ⊢ ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 } → ( ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐵 , 𝐴 } { 𝐵 , 𝑤 } ∈ 𝐸 ) )
44 37 43 ax-mp ⊢ ( ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐵 , 𝐴 } { 𝐵 , 𝑤 } ∈ 𝐸 )
45 42 44 sylibr ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 )
46 36 40 45 syl2an ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 )
47 26 46 jca ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) )
48 25 47 jca ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) )
49 preq1 ⊢ ( 𝑣 = 𝐴 → { 𝑣 , 𝐶 } = { 𝐴 , 𝐶 } )
50 49 eleq1d ⊢ ( 𝑣 = 𝐴 → ( { 𝑣 , 𝐶 } ∈ 𝐸 ↔ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
51 preq1 ⊢ ( 𝑣 = 𝐴 → { 𝑣 , 𝑤 } = { 𝐴 , 𝑤 } )
52 51 eleq1d ⊢ ( 𝑣 = 𝐴 → ( { 𝑣 , 𝑤 } ∈ 𝐸 ↔ { 𝐴 , 𝑤 } ∈ 𝐸 ) )
53 52 reubidv ⊢ ( 𝑣 = 𝐴 → ( ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) )
54 50 53 anbi12d ⊢ ( 𝑣 = 𝐴 → ( ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ) )
55 preq1 ⊢ ( 𝑣 = 𝐵 → { 𝑣 , 𝐶 } = { 𝐵 , 𝐶 } )
56 55 eleq1d ⊢ ( 𝑣 = 𝐵 → ( { 𝑣 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
57 preq1 ⊢ ( 𝑣 = 𝐵 → { 𝑣 , 𝑤 } = { 𝐵 , 𝑤 } )
58 57 eleq1d ⊢ ( 𝑣 = 𝐵 → ( { 𝑣 , 𝑤 } ∈ 𝐸 ↔ { 𝐵 , 𝑤 } ∈ 𝐸 ) )
59 58 reubidv ⊢ ( 𝑣 = 𝐵 → ( ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) )
60 56 59 anbi12d ⊢ ( 𝑣 = 𝐵 → ( ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) )
61 54 60 ralprg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) ) )
62 61 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) ) )
63 62 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) ) )
64 63 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) ) )
65 64 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐴 , 𝑤 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝐵 , 𝑤 } ∈ 𝐸 ) ) ) )
66 48 65 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) )
67 diftpsn3 ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
68 67 3adant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
69 reueq1 ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) )
70 68 69 syl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) )
71 70 anbi2d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
72 68 71 raleqbidv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
73 72 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
74 73 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
75 74 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ { 𝐴 , 𝐵 } ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ { 𝐴 , 𝐵 } { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
76 66 75 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
77 76 3mix3d ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
78 sneq ⊢ ( ℎ = 𝐴 → { ℎ } = { 𝐴 } )
79 78 difeq2d ⊢ ( ℎ = 𝐴 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) )
80 preq2 ⊢ ( ℎ = 𝐴 → { 𝑣 , ℎ } = { 𝑣 , 𝐴 } )
81 80 eleq1d ⊢ ( ℎ = 𝐴 → ( { 𝑣 , ℎ } ∈ 𝐸 ↔ { 𝑣 , 𝐴 } ∈ 𝐸 ) )
82 reueq1 ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
83 79 82 syl ⊢ ( ℎ = 𝐴 → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
84 81 83 anbi12d ⊢ ( ℎ = 𝐴 → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
85 79 84 raleqbidv ⊢ ( ℎ = 𝐴 → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
86 sneq ⊢ ( ℎ = 𝐵 → { ℎ } = { 𝐵 } )
87 86 difeq2d ⊢ ( ℎ = 𝐵 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) )
88 preq2 ⊢ ( ℎ = 𝐵 → { 𝑣 , ℎ } = { 𝑣 , 𝐵 } )
89 88 eleq1d ⊢ ( ℎ = 𝐵 → ( { 𝑣 , ℎ } ∈ 𝐸 ↔ { 𝑣 , 𝐵 } ∈ 𝐸 ) )
90 reueq1 ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
91 87 90 syl ⊢ ( ℎ = 𝐵 → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
92 89 91 anbi12d ⊢ ( ℎ = 𝐵 → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
93 87 92 raleqbidv ⊢ ( ℎ = 𝐵 → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
94 sneq ⊢ ( ℎ = 𝐶 → { ℎ } = { 𝐶 } )
95 94 difeq2d ⊢ ( ℎ = 𝐶 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) )
96 preq2 ⊢ ( ℎ = 𝐶 → { 𝑣 , ℎ } = { 𝑣 , 𝐶 } )
97 96 eleq1d ⊢ ( ℎ = 𝐶 → ( { 𝑣 , ℎ } ∈ 𝐸 ↔ { 𝑣 , 𝐶 } ∈ 𝐸 ) )
98 reueq1 ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
99 95 98 syl ⊢ ( ℎ = 𝐶 → ( ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
100 97 99 anbi12d ⊢ ( ℎ = 𝐶 → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
101 95 100 raleqbidv ⊢ ( ℎ = 𝐶 → ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
102 85 93 101 rextpg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
103 102 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
104 103 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
105 104 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ( ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( { 𝑣 , 𝐴 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( { 𝑣 , 𝐵 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ∨ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( { 𝑣 , 𝐶 } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
106 77 105 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
107 106 ex ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
108 6 107 sylbid ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
109 108 expcom ⊢ ( 𝐺 ∈ USGraph → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
110 109 com23 ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ FriendGraph → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
111 3 110 mpcom ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
112 111 com12 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
113 difeq1 ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝑉 ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) )
114 reueq1 ⊢ ( ( 𝑉 ∖ { ℎ } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) → ( ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
115 113 114 syl ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
116 115 anbi2d ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
117 113 116 raleqbidv ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
118 117 rexeqbi1dv ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ↔ ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
119 118 imbi2d ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ↔ ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
120 119 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ↔ ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑣 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
121 112 120 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )