Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgr3v Structured version   Visualization version   GIF version

Theorem frgr3v 28159
 Description: Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Revised by AV, 29-Mar-2021.)
Hypotheses
Ref Expression
frgr3v.v 𝑉 = (Vtx‘𝐺)
frgr3v.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
frgr3v (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))

Proof of Theorem frgr3v
Dummy variables 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgr3v.v . . . . . 6 𝑉 = (Vtx‘𝐺)
2 frgr3v.e . . . . . 6 𝐸 = (Edg‘𝐺)
31, 2isfrgr 28144 . . . . 5 (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
43a1i 11 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
5 id 22 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐵, 𝐶})
6 difeq1 4021 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘}))
7 reueq1 3325 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
86, 7raleqbidv 3319 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
95, 8raleqbidv 3319 . . . . . . 7 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
109anbi2d 631 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
1110baibd 543 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
1211adantl 485 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
134, 12bitrd 282 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
14 sneq 4532 . . . . . . . 8 (𝑘 = 𝐴 → {𝑘} = {𝐴})
1514difeq2d 4028 . . . . . . 7 (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
16 preq2 4627 . . . . . . . . . 10 (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴})
1716preq1d 4632 . . . . . . . . 9 (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}})
1817sseq1d 3923 . . . . . . . 8 (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
1918reubidv 3307 . . . . . . 7 (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
2015, 19raleqbidv 3319 . . . . . 6 (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
21 sneq 4532 . . . . . . . 8 (𝑘 = 𝐵 → {𝑘} = {𝐵})
2221difeq2d 4028 . . . . . . 7 (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
23 preq2 4627 . . . . . . . . . 10 (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵})
2423preq1d 4632 . . . . . . . . 9 (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}})
2524sseq1d 3923 . . . . . . . 8 (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2625reubidv 3307 . . . . . . 7 (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2722, 26raleqbidv 3319 . . . . . 6 (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
28 sneq 4532 . . . . . . . 8 (𝑘 = 𝐶 → {𝑘} = {𝐶})
2928difeq2d 4028 . . . . . . 7 (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
30 preq2 4627 . . . . . . . . . 10 (𝑘 = 𝐶 → {𝑥, 𝑘} = {𝑥, 𝐶})
3130preq1d 4632 . . . . . . . . 9 (𝑘 = 𝐶 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝑙}})
3231sseq1d 3923 . . . . . . . 8 (𝑘 = 𝐶 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3332reubidv 3307 . . . . . . 7 (𝑘 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3429, 33raleqbidv 3319 . . . . . 6 (𝑘 = 𝐶 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3520, 27, 34raltpg 4591 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
3635ad2antrr 725 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
37 tprot 4642 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
3837a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
3938difeq1d 4027 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
40 necom 3004 . . . . . . . . . . . 12 (𝐴𝐵𝐵𝐴)
4140biimpi 219 . . . . . . . . . . 11 (𝐴𝐵𝐵𝐴)
42 necom 3004 . . . . . . . . . . . 12 (𝐴𝐶𝐶𝐴)
4342biimpi 219 . . . . . . . . . . 11 (𝐴𝐶𝐶𝐴)
4441, 43anim12i 615 . . . . . . . . . 10 ((𝐴𝐵𝐴𝐶) → (𝐵𝐴𝐶𝐴))
45443adant3 1129 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐵𝐴𝐶𝐴))
46 diftpsn3 4692 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4745, 46syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4839, 47eqtrd 2793 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
4948raleqdv 3329 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
50 tprot 4642 . . . . . . . . . . 11 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
5150eqcomi 2767 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
5251a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
5352difeq1d 4027 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
54 id 22 . . . . . . . . . . 11 (𝐴𝐵𝐴𝐵)
55 necom 3004 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
5655biimpi 219 . . . . . . . . . . 11 (𝐵𝐶𝐶𝐵)
5754, 56anim12ci 616 . . . . . . . . . 10 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
58573adant2 1128 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐴𝐵))
59 diftpsn3 4692 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6058, 59syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6153, 60eqtrd 2793 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
6261raleqdv 3329 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
63 diftpsn3 4692 . . . . . . . 8 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
64633adant1 1127 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
6564raleqdv 3329 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
6649, 62, 653anbi123d 1433 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
6766ad2antlr 726 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
68 preq2 4627 . . . . . . . . . . 11 (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵})
6968preq2d 4633 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}})
7069sseq1d 3923 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
7170reubidv 3307 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
72 preq2 4627 . . . . . . . . . . 11 (𝑙 = 𝐶 → {𝑥, 𝑙} = {𝑥, 𝐶})
7372preq2d 4633 . . . . . . . . . 10 (𝑙 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐶}})
7473sseq1d 3923 . . . . . . . . 9 (𝑙 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7574reubidv 3307 . . . . . . . 8 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7671, 75ralprg 4589 . . . . . . 7 ((𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
77763adant1 1127 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
7872preq2d 4633 . . . . . . . . . . 11 (𝑙 = 𝐶 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐶}})
7978sseq1d 3923 . . . . . . . . . 10 (𝑙 = 𝐶 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
8079reubidv 3307 . . . . . . . . 9 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
81 preq2 4627 . . . . . . . . . . . 12 (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴})
8281preq2d 4633 . . . . . . . . . . 11 (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}})
8382sseq1d 3923 . . . . . . . . . 10 (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8483reubidv 3307 . . . . . . . . 9 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8580, 84ralprg 4589 . . . . . . . 8 ((𝐶𝑍𝐴𝑋) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8685ancoms 462 . . . . . . 7 ((𝐴𝑋𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
87863adant2 1128 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8881preq2d 4633 . . . . . . . . . 10 (𝑙 = 𝐴 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐴}})
8988sseq1d 3923 . . . . . . . . 9 (𝑙 = 𝐴 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9089reubidv 3307 . . . . . . . 8 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9168preq2d 4633 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐵}})
9291sseq1d 3923 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9392reubidv 3307 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9490, 93ralprg 4589 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
95943adant3 1129 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
9677, 87, 953anbi123d 1433 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9796ad2antrr 725 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9836, 67, 973bitrd 308 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
991, 2frgr3vlem2 28158 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
10099imp 410 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
101 simpll1 1209 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝑋)
102 simpll3 1211 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝑍)
103 simpll2 1210 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝑌)
104101, 102, 1033jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝑋𝐶𝑍𝐵𝑌))
105 simplr2 1213 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐶)
106 simplr1 1212 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐵)
10758simpld 498 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → 𝐶𝐵)
108107ad2antlr 726 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐵)
109105, 106, 1083jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝐶𝐴𝐵𝐶𝐵))
110 tpcomb 4644 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
1115, 110eqtrdi 2809 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐶, 𝐵})
112111anim1i 617 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
113112adantl 485 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
114 reueq1 3325 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
115110, 114mp1i 13 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
1161, 2frgr3vlem2 28158 . . . . . . . . 9 (((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) → ((𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
117116imp 410 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
118115, 117bitrd 282 . . . . . . 7 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
119104, 109, 113, 118syl21anc 836 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
120100, 119anbi12d 633 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
121103, 102, 1013jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐶𝑍𝐴𝑋))
122 simplr3 1214 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐶)
123106necomd 3006 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐴)
124105necomd 3006 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐴)
125122, 123, 1243jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐶𝐵𝐴𝐶𝐴))
12637eqeq2i 2771 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐶, 𝐴})
127126biimpi 219 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐶, 𝐴})
128127anim1i 617 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
129128adantl 485 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
130 reueq1 3325 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
13137, 130mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
1321, 2frgr3vlem2 28158 . . . . . . . . 9 (((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) → ((𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))))
133132imp 410 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
134131, 133bitrd 282 . . . . . . 7 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
135121, 125, 129, 134syl21anc 836 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
136103, 101, 1023jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐴𝑋𝐶𝑍))
137123, 122, 1053jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐴𝐵𝐶𝐴𝐶))
138 tpcoma 4643 . . . . . . . . . . 11 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
139138eqeq2i 2771 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶})
140139biimpi 219 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶})
141140anim1i 617 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
142141adantl 485 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
143 reueq1 3325 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
144138, 143mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
1451, 2frgr3vlem2 28158 . . . . . . . . 9 (((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) → ((𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
146145imp 410 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
147144, 146bitrd 282 . . . . . . 7 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
148136, 137, 142, 147syl21anc 836 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
149135, 148anbi12d 633 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
150102, 101, 1033jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝑍𝐴𝑋𝐵𝑌))
151124, 108, 1063jca 1125 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝐴𝐶𝐵𝐴𝐵))
15251eqeq2i 2771 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵})
153152biimpi 219 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵})
154153anim1i 617 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
155154adantl 485 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
156 reueq1 3325 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
15751, 156mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
1581, 2frgr3vlem2 28158 . . . . . . . . 9 (((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) → ((𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))))
159158imp 410 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
160157, 159bitrd 282 . . . . . . 7 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
161150, 151, 155, 160syl21anc 836 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
162 3anrev 1098 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) ↔ (𝐶𝑍𝐵𝑌𝐴𝑋))
163162biimpi 219 . . . . . . . 8 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (𝐶𝑍𝐵𝑌𝐴𝑋))
16455, 42, 403anbi123i 1152 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐶𝐴𝐵) ↔ (𝐶𝐵𝐶𝐴𝐵𝐴))
165164biimpi 219 . . . . . . . . 9 ((𝐵𝐶𝐴𝐶𝐴𝐵) → (𝐶𝐵𝐶𝐴𝐵𝐴))
1661653com13 1121 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐶𝐴𝐵𝐴))
167163, 166anim12i 615 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)))
168 tpcoma 4643 . . . . . . . . . . 11 {𝐵, 𝐶, 𝐴} = {𝐶, 𝐵, 𝐴}
16937, 168eqtri 2781 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴}
170169eqeq2i 2771 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐵, 𝐴})
171170biimpi 219 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐵, 𝐴})
172171anim1i 617 . . . . . . 7 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph))
173 reueq1 3325 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
174169, 173mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
1751, 2frgr3vlem2 28158 . . . . . . . . 9 (((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) → ((𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
176175imp 410 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
177174, 176bitrd 282 . . . . . . 7 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
178167, 172, 177syl2an 598 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
179161, 178anbi12d 633 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
180120, 149, 1793anbi123d 1433 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))))
181 prcom 4625 . . . . . . . . . 10 {𝐵, 𝐶} = {𝐶, 𝐵}
182181eleq1i 2842 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸)
183182anbi2i 625 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))
184183anbi2i 625 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
185 anandir 676 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
186184, 185bitr4i 281 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
187 prcom 4625 . . . . . . . . . 10 {𝐶, 𝐴} = {𝐴, 𝐶}
188187eleq1i 2842 . . . . . . . . 9 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸)
189188anbi2i 625 . . . . . . . 8 (({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
190189anbi2i 625 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
191 anandir 676 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
192190, 191bitr4i 281 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
193 prcom 4625 . . . . . . . . . 10 {𝐴, 𝐵} = {𝐵, 𝐴}
194193eleq1i 2842 . . . . . . . . 9 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸)
195194anbi2i 625 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))
196195anbi2i 625 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
197 anandir 676 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
198196, 197bitr4i 281 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
199186, 192, 1983anbi123i 1152 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)))
200 3anrot 1097 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
201 df-3an 1086 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
202 prcom 4625 . . . . . . . . 9 {𝐵, 𝐴} = {𝐴, 𝐵}
203202eleq1i 2842 . . . . . . . 8 ({𝐵, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
204 prcom 4625 . . . . . . . . 9 {𝐶, 𝐵} = {𝐵, 𝐶}
205204eleq1i 2842 . . . . . . . 8 ({𝐶, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
206 biid 264 . . . . . . . 8 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
207203, 205, 2063anbi123i 1152 . . . . . . 7 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
208200, 201, 2073bitr3i 304 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
209 df-3an 1086 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
210 biid 264 . . . . . . . 8 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
211 prcom 4625 . . . . . . . . 9 {𝐴, 𝐶} = {𝐶, 𝐴}
212211eleq1i 2842 . . . . . . . 8 ({𝐴, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
213210, 205, 2123anbi123i 1152 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
214209, 213bitr3i 280 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
215 df-3an 1086 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
216 3anrot 1097 . . . . . . . 8 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))
217 3anrot 1097 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
218 biid 264 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
219203, 218, 2123anbi123i 1152 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
220216, 217, 2193bitri 300 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
221215, 220bitr3i 280 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
222208, 214, 2213anbi123i 1152 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
223 df-3an 1086 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
224 anabs1 661 . . . . . 6 (((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
225 anidm 568 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
226223, 224, 2253bitri 300 . . . . 5 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
227199, 222, 2263bitri 300 . . . 4 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
228180, 227bitrdi 290 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
22913, 98, 2283bitrd 308 . 2 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
230229ex 416 1 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃!wreu 3072   ∖ cdif 3855   ⊆ wss 3858  {csn 4522  {cpr 4524  {ctp 4526  ‘cfv 6335  Vtxcvtx 26888  Edgcedg 26939  USGraphcusgr 27041   FriendGraph cfrgr 28142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-oadd 8116  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-2 11737  df-n0 11935  df-z 12021  df-uz 12283  df-fz 12940  df-hash 13741  df-edg 26940  df-umgr 26975  df-usgr 27043  df-frgr 28143 This theorem is referenced by:  3vfriswmgr  28162
 Copyright terms: Public domain W3C validator