Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3vfriswmgr Structured version   Visualization version   GIF version

Theorem 3vfriswmgr 41448
 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.)
Hypotheses
Ref Expression
3vfriswmgr.v 𝑉 = (Vtx‘𝐺)
3vfriswmgr.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
3vfriswmgr (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃𝑉𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
Distinct variable groups:   𝑤,𝐴   𝑤,𝐵   𝑤,𝐶   𝑤,𝐸   𝑤,𝐺   𝑤,𝑉   𝑤,𝑋   𝑤,𝑌   𝐴,,𝑣,𝑤   𝐵,,𝑣   𝐶,,𝑣   ,𝐸,𝑣   ,𝑉,𝑣
Allowed substitution hints:   𝐺(𝑣,)   𝑋(𝑣,)   𝑌(𝑣,)   𝑍(𝑤,𝑣,)

Proof of Theorem 3vfriswmgr
StepHypRef Expression
1 frgrusgr 41432 . . . 4 (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
2 3vfriswmgr.v . . . . . . . . . 10 𝑉 = (Vtx‘𝐺)
3 3vfriswmgr.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
42, 3frgr3v 41445 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph ) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
54exp4b 630 . . . . . . . 8 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐺 ∈ USGraph → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))))
653imp1 1272 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
7 prcom 4211 . . . . . . . . . . . . . . . . . 18 {𝐶, 𝐴} = {𝐴, 𝐶}
87eleq1i 2679 . . . . . . . . . . . . . . . . 17 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸)
98biimpi 205 . . . . . . . . . . . . . . . 16 ({𝐶, 𝐴} ∈ 𝐸 → {𝐴, 𝐶} ∈ 𝐸)
1093ad2ant3 1077 . . . . . . . . . . . . . . 15 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → {𝐴, 𝐶} ∈ 𝐸)
1110adantl 481 . . . . . . . . . . . . . 14 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → {𝐴, 𝐶} ∈ 𝐸)
12 simpl11 1129 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → 𝐴𝑋)
13 simpl12 1130 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → 𝐵𝑌)
14 simp1 1054 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝐵𝐴𝐶𝐵𝐶) → 𝐴𝐵)
15143ad2ant2 1076 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝐴𝐵)
1615adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → 𝐴𝐵)
1712, 13, 163jca 1235 . . . . . . . . . . . . . . . 16 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝐴𝑋𝐵𝑌𝐴𝐵))
18 simp3 1056 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝑉 = {𝐴, 𝐵, 𝐶})
1918anim1i 590 . . . . . . . . . . . . . . . 16 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph ))
2017, 19jca 553 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → ((𝐴𝑋𝐵𝑌𝐴𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph )))
21 simp1 1054 . . . . . . . . . . . . . . 15 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → {𝐴, 𝐵} ∈ 𝐸)
222, 33vfriswmgrlem 41447 . . . . . . . . . . . . . . . 16 (((𝐴𝑋𝐵𝑌𝐴𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph )) → ({𝐴, 𝐵} ∈ 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸))
2322imp 444 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐴𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph )) ∧ {𝐴, 𝐵} ∈ 𝐸) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸)
2420, 21, 23syl2an 493 . . . . . . . . . . . . . 14 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸)
2511, 24jca 553 . . . . . . . . . . . . 13 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸))
26 simpr2 1061 . . . . . . . . . . . . . 14 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → {𝐵, 𝐶} ∈ 𝐸)
27 necom 2835 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐵𝐵𝐴)
2827biimpi 205 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐵𝐵𝐴)
29283ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝐵𝐴𝐶𝐵𝐶) → 𝐵𝐴)
30293ad2ant2 1076 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝐵𝐴)
3130adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → 𝐵𝐴)
3213, 12, 313jca 1235 . . . . . . . . . . . . . . . 16 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝐵𝑌𝐴𝑋𝐵𝐴))
33 tpcoma 4229 . . . . . . . . . . . . . . . . . 18 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
3418, 33syl6eq 2660 . . . . . . . . . . . . . . . . 17 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝑉 = {𝐵, 𝐴, 𝐶})
3534anim1i 590 . . . . . . . . . . . . . . . 16 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph ))
3632, 35jca 553 . . . . . . . . . . . . . . 15 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → ((𝐵𝑌𝐴𝑋𝐵𝐴) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph )))
37 prcom 4211 . . . . . . . . . . . . . . . . . 18 {𝐴, 𝐵} = {𝐵, 𝐴}
3837eleq1i 2679 . . . . . . . . . . . . . . . . 17 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸)
3938biimpi 205 . . . . . . . . . . . . . . . 16 ({𝐴, 𝐵} ∈ 𝐸 → {𝐵, 𝐴} ∈ 𝐸)
40393ad2ant1 1075 . . . . . . . . . . . . . . 15 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → {𝐵, 𝐴} ∈ 𝐸)
412, 33vfriswmgrlem 41447 . . . . . . . . . . . . . . . . 17 (((𝐵𝑌𝐴𝑋𝐵𝐴) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph )) → ({𝐵, 𝐴} ∈ 𝐸 → ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ 𝐸))
4241imp 444 . . . . . . . . . . . . . . . 16 ((((𝐵𝑌𝐴𝑋𝐵𝐴) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph )) ∧ {𝐵, 𝐴} ∈ 𝐸) → ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ 𝐸)
43 reueq1 3117 . . . . . . . . . . . . . . . . 17 ({𝐴, 𝐵} = {𝐵, 𝐴} → (∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ 𝐸))
4437, 43ax-mp 5 . . . . . . . . . . . . . . . 16 (∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ 𝐸)
4542, 44sylibr 223 . . . . . . . . . . . . . . 15 ((((𝐵𝑌𝐴𝑋𝐵𝐴) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph )) ∧ {𝐵, 𝐴} ∈ 𝐸) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸)
4636, 40, 45syl2an 493 . . . . . . . . . . . . . 14 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸)
4726, 46jca 553 . . . . . . . . . . . . 13 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))
4825, 47jca 553 . . . . . . . . . . . 12 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸)))
49 preq1 4212 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝐴 → {𝑣, 𝐶} = {𝐴, 𝐶})
5049eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝐴 → ({𝑣, 𝐶} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸))
51 preq1 4212 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
5251eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝐴 → ({𝑣, 𝑤} ∈ 𝐸 ↔ {𝐴, 𝑤} ∈ 𝐸))
5352reubidv 3103 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝐴 → (∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸))
5450, 53anbi12d 743 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝐴 → (({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸)))
55 preq1 4212 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝐵 → {𝑣, 𝐶} = {𝐵, 𝐶})
5655eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝐵 → ({𝑣, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸))
57 preq1 4212 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
5857eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝐵 → ({𝑣, 𝑤} ∈ 𝐸 ↔ {𝐵, 𝑤} ∈ 𝐸))
5958reubidv 3103 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝐵 → (∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))
6056, 59anbi12d 743 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝐵 → (({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸)))
6154, 60ralprg 4181 . . . . . . . . . . . . . . . 16 ((𝐴𝑋𝐵𝑌) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))))
62613adant3 1074 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))))
63623ad2ant1 1075 . . . . . . . . . . . . . 14 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))))
6463adantr 480 . . . . . . . . . . . . 13 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))))
6564adantr 480 . . . . . . . . . . . 12 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸) ↔ (({𝐴, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸) ∧ ({𝐵, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ 𝐸))))
6648, 65mpbird 246 . . . . . . . . . . 11 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸))
67 diftpsn3 4273 . . . . . . . . . . . . . . . 16 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
68673adant1 1072 . . . . . . . . . . . . . . 15 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
69 reueq1 3117 . . . . . . . . . . . . . . . . 17 (({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵} → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸))
7068, 69syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸))
7170anbi2d 736 . . . . . . . . . . . . . . 15 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸) ↔ ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸)))
7268, 71raleqbidv 3129 . . . . . . . . . . . . . 14 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸)))
73723ad2ant2 1076 . . . . . . . . . . . . 13 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸)))
7473adantr 480 . . . . . . . . . . . 12 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸)))
7574adantr 480 . . . . . . . . . . 11 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ 𝐸)))
7666, 75mpbird 246 . . . . . . . . . 10 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))
77763mix3d 1231 . . . . . . . . 9 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸)))
78 sneq 4135 . . . . . . . . . . . . . . 15 ( = 𝐴 → {} = {𝐴})
7978difeq2d 3690 . . . . . . . . . . . . . 14 ( = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
80 preq2 4213 . . . . . . . . . . . . . . . 16 ( = 𝐴 → {𝑣, } = {𝑣, 𝐴})
8180eleq1d 2672 . . . . . . . . . . . . . . 15 ( = 𝐴 → ({𝑣, } ∈ 𝐸 ↔ {𝑣, 𝐴} ∈ 𝐸))
82 reueq1 3117 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸))
8379, 82syl 17 . . . . . . . . . . . . . . 15 ( = 𝐴 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸))
8481, 83anbi12d 743 . . . . . . . . . . . . . 14 ( = 𝐴 → (({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸)))
8579, 84raleqbidv 3129 . . . . . . . . . . . . 13 ( = 𝐴 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸)))
86 sneq 4135 . . . . . . . . . . . . . . 15 ( = 𝐵 → {} = {𝐵})
8786difeq2d 3690 . . . . . . . . . . . . . 14 ( = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
88 preq2 4213 . . . . . . . . . . . . . . . 16 ( = 𝐵 → {𝑣, } = {𝑣, 𝐵})
8988eleq1d 2672 . . . . . . . . . . . . . . 15 ( = 𝐵 → ({𝑣, } ∈ 𝐸 ↔ {𝑣, 𝐵} ∈ 𝐸))
90 reueq1 3117 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸))
9187, 90syl 17 . . . . . . . . . . . . . . 15 ( = 𝐵 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸))
9289, 91anbi12d 743 . . . . . . . . . . . . . 14 ( = 𝐵 → (({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸)))
9387, 92raleqbidv 3129 . . . . . . . . . . . . 13 ( = 𝐵 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸)))
94 sneq 4135 . . . . . . . . . . . . . . 15 ( = 𝐶 → {} = {𝐶})
9594difeq2d 3690 . . . . . . . . . . . . . 14 ( = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
96 preq2 4213 . . . . . . . . . . . . . . . 16 ( = 𝐶 → {𝑣, } = {𝑣, 𝐶})
9796eleq1d 2672 . . . . . . . . . . . . . . 15 ( = 𝐶 → ({𝑣, } ∈ 𝐸 ↔ {𝑣, 𝐶} ∈ 𝐸))
98 reueq1 3117 . . . . . . . . . . . . . . . 16 (({𝐴, 𝐵, 𝐶} ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))
9995, 98syl 17 . . . . . . . . . . . . . . 15 ( = 𝐶 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))
10097, 99anbi12d 743 . . . . . . . . . . . . . 14 ( = 𝐶 → (({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸)))
10195, 100raleqbidv 3129 . . . . . . . . . . . . 13 ( = 𝐶 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸)))
10285, 93, 101rextpg 4184 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))))
1031023ad2ant1 1075 . . . . . . . . . . 11 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))))
104103adantr 480 . . . . . . . . . 10 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))))
105104adantr 480 . . . . . . . . 9 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → (∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ 𝐸))))
10677, 105mpbird 246 . . . . . . . 8 (((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))
107106ex 449 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
1086, 107sylbid 229 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐺 ∈ USGraph ) → (𝐺 ∈ FriendGraph → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
109108expcom 450 . . . . 5 (𝐺 ∈ USGraph → (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))))
110109com23 84 . . . 4 (𝐺 ∈ USGraph → (𝐺 ∈ FriendGraph → (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))))
1111, 110mpcom 37 . . 3 (𝐺 ∈ FriendGraph → (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
112111com12 32 . 2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
113 difeq1 3683 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {}))
114 reueq1 3117 . . . . . . . 8 ((𝑉 ∖ {}) = ({𝐴, 𝐵, 𝐶} ∖ {}) → (∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))
115113, 114syl 17 . . . . . . 7 (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))
116115anbi2d 736 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → (({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
117113, 116raleqbidv 3129 . . . . 5 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
118117rexeqbi1dv 3124 . . . 4 (𝑉 = {𝐴, 𝐵, 𝐶} → (∃𝑉𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸) ↔ ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
119118imbi2d 329 . . 3 (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝐺 ∈ FriendGraph → ∃𝑉𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸)) ↔ (𝐺 ∈ FriendGraph → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))))
1201193ad2ant3 1077 . 2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ((𝐺 ∈ FriendGraph → ∃𝑉𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸)) ↔ (𝐺 ∈ FriendGraph → ∃ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {}){𝑣, 𝑤} ∈ 𝐸))))
121112, 120mpbird 246 1 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃𝑉𝑣 ∈ (𝑉 ∖ {})({𝑣, } ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {}){𝑣, 𝑤} ∈ 𝐸)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898   ∖ cdif 3537  {csn 4125  {cpr 4127  {ctp 4129  ‘cfv 5804  Vtxcvtx 25673  Edgcedga 25792   USGraph cusgr 40379   FriendGraph cfrgr 41428 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980  df-umgr 25750  df-edga 25793  df-usgr 40381  df-frgr 41429 This theorem is referenced by:  1to3vfriswmgr  41450
 Copyright terms: Public domain W3C validator