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

Theorem frgr3v 27255
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, 2frgrusgrfrcond 27239 . . . . 5 (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
43a1i 11 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
5 id 22 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐵, 𝐶})
6 difeq1 3754 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘}))
7 reueq1 3170 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
86, 7raleqbidv 3182 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
95, 8raleqbidv 3182 . . . . . . 7 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
109anbi2d 740 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
1110baibd 968 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
1211adantl 481 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
134, 12bitrd 268 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
14 sneq 4220 . . . . . . . 8 (𝑘 = 𝐴 → {𝑘} = {𝐴})
1514difeq2d 3761 . . . . . . 7 (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
16 preq2 4301 . . . . . . . . . 10 (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴})
1716preq1d 4306 . . . . . . . . 9 (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}})
1817sseq1d 3665 . . . . . . . 8 (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
1918reubidv 3156 . . . . . . 7 (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
2015, 19raleqbidv 3182 . . . . . 6 (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
21 sneq 4220 . . . . . . . 8 (𝑘 = 𝐵 → {𝑘} = {𝐵})
2221difeq2d 3761 . . . . . . 7 (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
23 preq2 4301 . . . . . . . . . 10 (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵})
2423preq1d 4306 . . . . . . . . 9 (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}})
2524sseq1d 3665 . . . . . . . 8 (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2625reubidv 3156 . . . . . . 7 (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2722, 26raleqbidv 3182 . . . . . 6 (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
28 sneq 4220 . . . . . . . 8 (𝑘 = 𝐶 → {𝑘} = {𝐶})
2928difeq2d 3761 . . . . . . 7 (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
30 preq2 4301 . . . . . . . . . 10 (𝑘 = 𝐶 → {𝑥, 𝑘} = {𝑥, 𝐶})
3130preq1d 4306 . . . . . . . . 9 (𝑘 = 𝐶 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝑙}})
3231sseq1d 3665 . . . . . . . 8 (𝑘 = 𝐶 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3332reubidv 3156 . . . . . . 7 (𝑘 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3429, 33raleqbidv 3182 . . . . . 6 (𝑘 = 𝐶 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3520, 27, 34raltpg 4268 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
3635ad2antrr 762 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
37 tprot 4316 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
3837a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
3938difeq1d 3760 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
40 necom 2876 . . . . . . . . . . . 12 (𝐴𝐵𝐵𝐴)
4140biimpi 206 . . . . . . . . . . 11 (𝐴𝐵𝐵𝐴)
42 necom 2876 . . . . . . . . . . . 12 (𝐴𝐶𝐶𝐴)
4342biimpi 206 . . . . . . . . . . 11 (𝐴𝐶𝐶𝐴)
4441, 43anim12i 589 . . . . . . . . . 10 ((𝐴𝐵𝐴𝐶) → (𝐵𝐴𝐶𝐴))
45443adant3 1101 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐵𝐴𝐶𝐴))
46 diftpsn3 4364 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4745, 46syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4839, 47eqtrd 2685 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
4948raleqdv 3174 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
50 tprot 4316 . . . . . . . . . . 11 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
5150eqcomi 2660 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
5251a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
5352difeq1d 3760 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
54 id 22 . . . . . . . . . . 11 (𝐴𝐵𝐴𝐵)
55 necom 2876 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
5655biimpi 206 . . . . . . . . . . 11 (𝐵𝐶𝐶𝐵)
5754, 56anim12ci 590 . . . . . . . . . 10 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
58573adant2 1100 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐴𝐵))
59 diftpsn3 4364 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6058, 59syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6153, 60eqtrd 2685 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
6261raleqdv 3174 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
63 diftpsn3 4364 . . . . . . . 8 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
64633adant1 1099 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
6564raleqdv 3174 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
6649, 62, 653anbi123d 1439 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
6766ad2antlr 763 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
68 preq2 4301 . . . . . . . . . . 11 (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵})
6968preq2d 4307 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}})
7069sseq1d 3665 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
7170reubidv 3156 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
72 preq2 4301 . . . . . . . . . . 11 (𝑙 = 𝐶 → {𝑥, 𝑙} = {𝑥, 𝐶})
7372preq2d 4307 . . . . . . . . . 10 (𝑙 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐶}})
7473sseq1d 3665 . . . . . . . . 9 (𝑙 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7574reubidv 3156 . . . . . . . 8 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7671, 75ralprg 4266 . . . . . . 7 ((𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
77763adant1 1099 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
7872preq2d 4307 . . . . . . . . . . 11 (𝑙 = 𝐶 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐶}})
7978sseq1d 3665 . . . . . . . . . 10 (𝑙 = 𝐶 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
8079reubidv 3156 . . . . . . . . 9 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
81 preq2 4301 . . . . . . . . . . . 12 (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴})
8281preq2d 4307 . . . . . . . . . . 11 (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}})
8382sseq1d 3665 . . . . . . . . . 10 (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8483reubidv 3156 . . . . . . . . 9 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8580, 84ralprg 4266 . . . . . . . 8 ((𝐶𝑍𝐴𝑋) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8685ancoms 468 . . . . . . 7 ((𝐴𝑋𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
87863adant2 1100 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8881preq2d 4307 . . . . . . . . . 10 (𝑙 = 𝐴 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐴}})
8988sseq1d 3665 . . . . . . . . 9 (𝑙 = 𝐴 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9089reubidv 3156 . . . . . . . 8 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9168preq2d 4307 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐵}})
9291sseq1d 3665 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9392reubidv 3156 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9490, 93ralprg 4266 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
95943adant3 1101 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
9677, 87, 953anbi123d 1439 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9796ad2antrr 762 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9836, 67, 973bitrd 294 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
991, 2frgr3vlem2 27254 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
10099imp 444 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
101 simpll1 1120 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝑋)
102 simpll3 1122 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝑍)
103 simpll2 1121 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝑌)
104101, 102, 1033jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝑋𝐶𝑍𝐵𝑌))
105 simplr2 1124 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐶)
106 simplr1 1123 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐵)
10758simpld 474 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → 𝐶𝐵)
108107ad2antlr 763 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐵)
109105, 106, 1083jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝐶𝐴𝐵𝐶𝐵))
110 tpcomb 4318 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
1115, 110syl6eq 2701 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐶, 𝐵})
112111anim1i 591 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
113112adantl 481 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
114 reueq1 3170 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
115110, 114mp1i 13 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
1161, 2frgr3vlem2 27254 . . . . . . . . 9 (((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) → ((𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
117116imp 444 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
118115, 117bitrd 268 . . . . . . 7 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
119104, 109, 113, 118syl21anc 1365 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
120100, 119anbi12d 747 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
121103, 102, 1013jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐶𝑍𝐴𝑋))
122 simplr3 1125 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐶)
123106necomd 2878 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐴)
124105necomd 2878 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐴)
125122, 123, 1243jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐶𝐵𝐴𝐶𝐴))
12637eqeq2i 2663 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐶, 𝐴})
127126biimpi 206 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐶, 𝐴})
128127anim1i 591 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
129128adantl 481 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
130 reueq1 3170 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
13137, 130mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
1321, 2frgr3vlem2 27254 . . . . . . . . 9 (((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) → ((𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))))
133132imp 444 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
134131, 133bitrd 268 . . . . . . 7 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
135121, 125, 129, 134syl21anc 1365 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
136103, 101, 1023jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐴𝑋𝐶𝑍))
137123, 122, 1053jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐴𝐵𝐶𝐴𝐶))
138 tpcoma 4317 . . . . . . . . . . 11 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
139138eqeq2i 2663 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶})
140139biimpi 206 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶})
141140anim1i 591 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
142141adantl 481 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
143 reueq1 3170 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
144138, 143mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
1451, 2frgr3vlem2 27254 . . . . . . . . 9 (((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) → ((𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
146145imp 444 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
147144, 146bitrd 268 . . . . . . 7 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
148136, 137, 142, 147syl21anc 1365 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
149135, 148anbi12d 747 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
150102, 101, 1033jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝑍𝐴𝑋𝐵𝑌))
151124, 108, 1063jca 1261 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝐴𝐶𝐵𝐴𝐵))
15251eqeq2i 2663 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵})
153152biimpi 206 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵})
154153anim1i 591 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
155154adantl 481 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
156 reueq1 3170 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
15751, 156mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
1581, 2frgr3vlem2 27254 . . . . . . . . 9 (((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) → ((𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))))
159158imp 444 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
160157, 159bitrd 268 . . . . . . 7 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
161150, 151, 155, 160syl21anc 1365 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
162 3anrev 1067 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) ↔ (𝐶𝑍𝐵𝑌𝐴𝑋))
163162biimpi 206 . . . . . . . 8 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (𝐶𝑍𝐵𝑌𝐴𝑋))
16455, 42, 403anbi123i 1270 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐶𝐴𝐵) ↔ (𝐶𝐵𝐶𝐴𝐵𝐴))
165164biimpi 206 . . . . . . . . 9 ((𝐵𝐶𝐴𝐶𝐴𝐵) → (𝐶𝐵𝐶𝐴𝐵𝐴))
1661653com13 1289 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐶𝐴𝐵𝐴))
167163, 166anim12i 589 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)))
168 tpcoma 4317 . . . . . . . . . . 11 {𝐵, 𝐶, 𝐴} = {𝐶, 𝐵, 𝐴}
16937, 168eqtri 2673 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴}
170169eqeq2i 2663 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐵, 𝐴})
171170biimpi 206 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐵, 𝐴})
172171anim1i 591 . . . . . . 7 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph))
173 reueq1 3170 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
174169, 173mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
1751, 2frgr3vlem2 27254 . . . . . . . . 9 (((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) → ((𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
176175imp 444 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
177174, 176bitrd 268 . . . . . . 7 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
178167, 172, 177syl2an 493 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
179161, 178anbi12d 747 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
180120, 149, 1793anbi123d 1439 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))))
181 prcom 4299 . . . . . . . . . 10 {𝐵, 𝐶} = {𝐶, 𝐵}
182181eleq1i 2721 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸)
183182anbi2i 730 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))
184183anbi2i 730 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
185 anandir 889 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
186184, 185bitr4i 267 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
187 prcom 4299 . . . . . . . . . 10 {𝐶, 𝐴} = {𝐴, 𝐶}
188187eleq1i 2721 . . . . . . . . 9 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸)
189188anbi2i 730 . . . . . . . 8 (({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
190189anbi2i 730 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
191 anandir 889 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
192190, 191bitr4i 267 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
193 prcom 4299 . . . . . . . . . 10 {𝐴, 𝐵} = {𝐵, 𝐴}
194193eleq1i 2721 . . . . . . . . 9 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸)
195194anbi2i 730 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))
196195anbi2i 730 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
197 anandir 889 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
198196, 197bitr4i 267 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
199186, 192, 1983anbi123i 1270 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)))
200 3anrot 1060 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
201 df-3an 1056 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
202 prcom 4299 . . . . . . . . 9 {𝐵, 𝐴} = {𝐴, 𝐵}
203202eleq1i 2721 . . . . . . . 8 ({𝐵, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
204 prcom 4299 . . . . . . . . 9 {𝐶, 𝐵} = {𝐵, 𝐶}
205204eleq1i 2721 . . . . . . . 8 ({𝐶, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
206 biid 251 . . . . . . . 8 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
207203, 205, 2063anbi123i 1270 . . . . . . 7 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
208200, 201, 2073bitr3i 290 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
209 df-3an 1056 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
210 biid 251 . . . . . . . 8 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
211 prcom 4299 . . . . . . . . 9 {𝐴, 𝐶} = {𝐶, 𝐴}
212211eleq1i 2721 . . . . . . . 8 ({𝐴, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
213210, 205, 2123anbi123i 1270 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
214209, 213bitr3i 266 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
215 df-3an 1056 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
216 3anrot 1060 . . . . . . . 8 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))
217 3anrot 1060 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
218 biid 251 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
219203, 218, 2123anbi123i 1270 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
220216, 217, 2193bitri 286 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
221215, 220bitr3i 266 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
222208, 214, 2213anbi123i 1270 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
223 df-3an 1056 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
224 anabs1 867 . . . . . 6 (((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
225 anidm 677 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
226223, 224, 2253bitri 286 . . . . 5 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
227199, 222, 2263bitri 286 . . . 4 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
228180, 227syl6bb 276 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
22913, 98, 2283bitrd 294 . 2 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
230229ex 449 1 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  ∃!wreu 2943  cdif 3604  wss 3607  {csn 4210  {cpr 4212  {ctp 4214  cfv 5926  Vtxcvtx 25919  Edgcedg 25984  USGraphcusgr 26089   FriendGraph cfrgr 27236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158  df-edg 25985  df-umgr 26023  df-usgr 26091  df-frgr 27237
This theorem is referenced by:  3vfriswmgr  27258
  Copyright terms: Public domain W3C validator