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 → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )