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

Theorem frgr3v 27513
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 27497 . . . . 5 (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
43a1i 11 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
5 id 22 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐵, 𝐶})
6 difeq1 3883 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑘}))
7 reueq1 3288 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
86, 7raleqbidv 3300 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
95, 8raleqbidv 3300 . . . . . . 7 (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
109anbi2d 622 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)))
1110baibd 535 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
1211adantl 473 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((𝐺 ∈ USGraph ∧ ∀𝑘𝑉𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
134, 12bitrd 270 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
14 sneq 4344 . . . . . . . 8 (𝑘 = 𝐴 → {𝑘} = {𝐴})
1514difeq2d 3890 . . . . . . 7 (𝑘 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
16 preq2 4424 . . . . . . . . . 10 (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴})
1716preq1d 4429 . . . . . . . . 9 (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}})
1817sseq1d 3792 . . . . . . . 8 (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
1918reubidv 3274 . . . . . . 7 (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
2015, 19raleqbidv 3300 . . . . . 6 (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
21 sneq 4344 . . . . . . . 8 (𝑘 = 𝐵 → {𝑘} = {𝐵})
2221difeq2d 3890 . . . . . . 7 (𝑘 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
23 preq2 4424 . . . . . . . . . 10 (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵})
2423preq1d 4429 . . . . . . . . 9 (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}})
2524sseq1d 3792 . . . . . . . 8 (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2625reubidv 3274 . . . . . . 7 (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
2722, 26raleqbidv 3300 . . . . . 6 (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
28 sneq 4344 . . . . . . . 8 (𝑘 = 𝐶 → {𝑘} = {𝐶})
2928difeq2d 3890 . . . . . . 7 (𝑘 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑘}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
30 preq2 4424 . . . . . . . . . 10 (𝑘 = 𝐶 → {𝑥, 𝑘} = {𝑥, 𝐶})
3130preq1d 4429 . . . . . . . . 9 (𝑘 = 𝐶 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝑙}})
3231sseq1d 3792 . . . . . . . 8 (𝑘 = 𝐶 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3332reubidv 3274 . . . . . . 7 (𝑘 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3429, 33raleqbidv 3300 . . . . . 6 (𝑘 = 𝐶 → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
3520, 27, 34raltpg 4392 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
3635ad2antrr 717 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
37 tprot 4439 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
3837a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
3938difeq1d 3889 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
40 necom 2990 . . . . . . . . . . . 12 (𝐴𝐵𝐵𝐴)
4140biimpi 207 . . . . . . . . . . 11 (𝐴𝐵𝐵𝐴)
42 necom 2990 . . . . . . . . . . . 12 (𝐴𝐶𝐶𝐴)
4342biimpi 207 . . . . . . . . . . 11 (𝐴𝐶𝐶𝐴)
4441, 43anim12i 606 . . . . . . . . . 10 ((𝐴𝐵𝐴𝐶) → (𝐵𝐴𝐶𝐴))
45443adant3 1162 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐵𝐴𝐶𝐴))
46 diftpsn3 4487 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4745, 46syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
4839, 47eqtrd 2799 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
4948raleqdv 3292 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸))
50 tprot 4439 . . . . . . . . . . 11 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
5150eqcomi 2774 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
5251a1i 11 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
5352difeq1d 3889 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
54 id 22 . . . . . . . . . . 11 (𝐴𝐵𝐴𝐵)
55 necom 2990 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
5655biimpi 207 . . . . . . . . . . 11 (𝐵𝐶𝐶𝐵)
5754, 56anim12ci 607 . . . . . . . . . 10 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
58573adant2 1161 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐴𝐵))
59 diftpsn3 4487 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6058, 59syl 17 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6153, 60eqtrd 2799 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
6261raleqdv 3292 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸))
63 diftpsn3 4487 . . . . . . . 8 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
64633adant1 1160 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
6564raleqdv 3292 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸))
6649, 62, 653anbi123d 1560 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
6766ad2antlr 718 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸)))
68 preq2 4424 . . . . . . . . . . 11 (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵})
6968preq2d 4430 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}})
7069sseq1d 3792 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
7170reubidv 3274 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸))
72 preq2 4424 . . . . . . . . . . 11 (𝑙 = 𝐶 → {𝑥, 𝑙} = {𝑥, 𝐶})
7372preq2d 4430 . . . . . . . . . 10 (𝑙 = 𝐶 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐶}})
7473sseq1d 3792 . . . . . . . . 9 (𝑙 = 𝐶 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7574reubidv 3274 . . . . . . . 8 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
7671, 75ralprg 4390 . . . . . . 7 ((𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
77763adant1 1160 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸)))
7872preq2d 4430 . . . . . . . . . . 11 (𝑙 = 𝐶 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐶}})
7978sseq1d 3792 . . . . . . . . . 10 (𝑙 = 𝐶 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
8079reubidv 3274 . . . . . . . . 9 (𝑙 = 𝐶 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
81 preq2 4424 . . . . . . . . . . . 12 (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴})
8281preq2d 4430 . . . . . . . . . . 11 (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}})
8382sseq1d 3792 . . . . . . . . . 10 (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8483reubidv 3274 . . . . . . . . 9 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
8580, 84ralprg 4390 . . . . . . . 8 ((𝐶𝑍𝐴𝑋) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8685ancoms 450 . . . . . . 7 ((𝐴𝑋𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
87863adant2 1161 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸)))
8881preq2d 4430 . . . . . . . . . 10 (𝑙 = 𝐴 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐴}})
8988sseq1d 3792 . . . . . . . . 9 (𝑙 = 𝐴 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9089reubidv 3274 . . . . . . . 8 (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
9168preq2d 4430 . . . . . . . . . 10 (𝑙 = 𝐵 → {{𝑥, 𝐶}, {𝑥, 𝑙}} = {{𝑥, 𝐶}, {𝑥, 𝐵}})
9291sseq1d 3792 . . . . . . . . 9 (𝑙 = 𝐵 → ({{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9392reubidv 3274 . . . . . . . 8 (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
9490, 93ralprg 4390 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
95943adant3 1162 . . . . . 6 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)))
9677, 87, 953anbi123d 1560 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9796ad2antrr 717 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∀𝑙 ∈ {𝐵, 𝐶}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐶, 𝐴}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ 𝐸 ∧ ∀𝑙 ∈ {𝐴, 𝐵}∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝑙}} ⊆ 𝐸) ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
9836, 67, 973bitrd 296 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∀𝑘 ∈ {𝐴, 𝐵, 𝐶}∀𝑙 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸 ↔ ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))))
991, 2frgr3vlem2 27512 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
10099imp 395 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
101 simpll1 1269 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝑋)
102 simpll3 1273 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝑍)
103 simpll2 1271 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝑌)
104101, 102, 1033jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝑋𝐶𝑍𝐵𝑌))
105 simplr2 1277 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐶)
106 simplr1 1275 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐴𝐵)
10758simpld 488 . . . . . . . . 9 ((𝐴𝐵𝐴𝐶𝐵𝐶) → 𝐶𝐵)
108107ad2antlr 718 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐵)
109105, 106, 1083jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐴𝐶𝐴𝐵𝐶𝐵))
110 tpcomb 4441 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵}
1115, 110syl6eq 2815 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐴, 𝐶, 𝐵})
112111anim1i 608 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
113112adantl 473 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph))
114 reueq1 3288 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐴, 𝐶, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
115110, 114mp1i 13 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸))
1161, 2frgr3vlem2 27512 . . . . . . . . 9 (((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) → ((𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
117116imp 395 . . . . . . . 8 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐶, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
118115, 117bitrd 270 . . . . . . 7 ((((𝐴𝑋𝐶𝑍𝐵𝑌) ∧ (𝐴𝐶𝐴𝐵𝐶𝐵)) ∧ (𝑉 = {𝐴, 𝐶, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
119104, 109, 113, 118syl21anc 866 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)))
120100, 119anbi12d 624 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))))
121103, 102, 1013jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐶𝑍𝐴𝑋))
122 simplr3 1279 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐶)
123106necomd 2992 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐵𝐴)
124105necomd 2992 . . . . . . . 8 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → 𝐶𝐴)
125122, 123, 1243jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐶𝐵𝐴𝐶𝐴))
12637eqeq2i 2777 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐶, 𝐴})
127126biimpi 207 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐶, 𝐴})
128127anim1i 608 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
129128adantl 473 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph))
130 reueq1 3288 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
13137, 130mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸))
1321, 2frgr3vlem2 27512 . . . . . . . . 9 (((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) → ((𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))))
133132imp 395 . . . . . . . 8 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐶, 𝐴} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
134131, 133bitrd 270 . . . . . . 7 ((((𝐵𝑌𝐶𝑍𝐴𝑋) ∧ (𝐵𝐶𝐵𝐴𝐶𝐴)) ∧ (𝑉 = {𝐵, 𝐶, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
135121, 125, 129, 134syl21anc 866 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
136103, 101, 1023jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝑌𝐴𝑋𝐶𝑍))
137123, 122, 1053jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐵𝐴𝐵𝐶𝐴𝐶))
138 tpcoma 4440 . . . . . . . . . . 11 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶}
139138eqeq2i 2777 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶})
140139biimpi 207 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶})
141140anim1i 608 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
142141adantl 473 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph))
143 reueq1 3288 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
144138, 143mp1i 13 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸))
1451, 2frgr3vlem2 27512 . . . . . . . . 9 (((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) → ((𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
146145imp 395 . . . . . . . 8 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐵, 𝐴, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
147144, 146bitrd 270 . . . . . . 7 ((((𝐵𝑌𝐴𝑋𝐶𝑍) ∧ (𝐵𝐴𝐵𝐶𝐴𝐶)) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
148136, 137, 142, 147syl21anc 866 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
149135, 148anbi12d 624 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
150102, 101, 1033jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝑍𝐴𝑋𝐵𝑌))
151124, 108, 1063jca 1158 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐶𝐴𝐶𝐵𝐴𝐵))
15251eqeq2i 2777 . . . . . . . . . 10 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵})
153152biimpi 207 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵})
154153anim1i 608 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
155154adantl 473 . . . . . . 7 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph))
156 reueq1 3288 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
15751, 156mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸))
1581, 2frgr3vlem2 27512 . . . . . . . . 9 (((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) → ((𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))))
159158imp 395 . . . . . . . 8 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐴, 𝐵} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
160157, 159bitrd 270 . . . . . . 7 ((((𝐶𝑍𝐴𝑋𝐵𝑌) ∧ (𝐶𝐴𝐶𝐵𝐴𝐵)) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
161150, 151, 155, 160syl21anc 866 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ↔ ({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
162 3anrev 1126 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) ↔ (𝐶𝑍𝐵𝑌𝐴𝑋))
163162biimpi 207 . . . . . . . 8 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (𝐶𝑍𝐵𝑌𝐴𝑋))
16455, 42, 403anbi123i 1194 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐶𝐴𝐵) ↔ (𝐶𝐵𝐶𝐴𝐵𝐴))
165164biimpi 207 . . . . . . . . 9 ((𝐵𝐶𝐴𝐶𝐴𝐵) → (𝐶𝐵𝐶𝐴𝐵𝐴))
1661653com13 1154 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (𝐶𝐵𝐶𝐴𝐵𝐴))
167163, 166anim12i 606 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)))
168 tpcoma 4440 . . . . . . . . . . 11 {𝐵, 𝐶, 𝐴} = {𝐶, 𝐵, 𝐴}
16937, 168eqtri 2787 . . . . . . . . . 10 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴}
170169eqeq2i 2777 . . . . . . . . 9 (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐵, 𝐴})
171170biimpi 207 . . . . . . . 8 (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐵, 𝐴})
172171anim1i 608 . . . . . . 7 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph))
173 reueq1 3288 . . . . . . . . 9 ({𝐴, 𝐵, 𝐶} = {𝐶, 𝐵, 𝐴} → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
174169, 173mp1i 13 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸))
1751, 2frgr3vlem2 27512 . . . . . . . . 9 (((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) → ((𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
176175imp 395 . . . . . . . 8 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐶, 𝐵, 𝐴} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
177174, 176bitrd 270 . . . . . . 7 ((((𝐶𝑍𝐵𝑌𝐴𝑋) ∧ (𝐶𝐵𝐶𝐴𝐵𝐴)) ∧ (𝑉 = {𝐶, 𝐵, 𝐴} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
178167, 172, 177syl2an 589 . . . . . 6 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))
179161, 178anbi12d 624 . . . . 5 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))))
180120, 149, 1793anbi123d 1560 . . . 4 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)))))
181 prcom 4422 . . . . . . . . . 10 {𝐵, 𝐶} = {𝐶, 𝐵}
182181eleq1i 2835 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐵} ∈ 𝐸)
183182anbi2i 616 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))
184183anbi2i 616 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
185 anandir 667 . . . . . . 7 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))
186184, 185bitr4i 269 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
187 prcom 4422 . . . . . . . . . 10 {𝐶, 𝐴} = {𝐴, 𝐶}
188187eleq1i 2835 . . . . . . . . 9 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐶} ∈ 𝐸)
189188anbi2i 616 . . . . . . . 8 (({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
190189anbi2i 616 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
191 anandir 667 . . . . . . 7 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸)))
192190, 191bitr4i 269 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
193 prcom 4422 . . . . . . . . . 10 {𝐴, 𝐵} = {𝐵, 𝐴}
194193eleq1i 2835 . . . . . . . . 9 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐴} ∈ 𝐸)
195194anbi2i 616 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸))
196195anbi2i 616 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
197 anandir 667 . . . . . . 7 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸)))
198196, 197bitr4i 269 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸)) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
199186, 192, 1983anbi123i 1194 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)))
200 3anrot 1122 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
201 df-3an 1109 . . . . . . 7 (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ (({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸))
202 prcom 4422 . . . . . . . . 9 {𝐵, 𝐴} = {𝐴, 𝐵}
203202eleq1i 2835 . . . . . . . 8 ({𝐵, 𝐴} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
204 prcom 4422 . . . . . . . . 9 {𝐶, 𝐵} = {𝐵, 𝐶}
205204eleq1i 2835 . . . . . . . 8 ({𝐶, 𝐵} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
206 biid 252 . . . . . . . 8 ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
207203, 205, 2063anbi123i 1194 . . . . . . 7 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
208200, 201, 2073bitr3i 292 . . . . . 6 ((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
209 df-3an 1109 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸))
210 biid 252 . . . . . . . 8 ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ 𝐸)
211 prcom 4422 . . . . . . . . 9 {𝐴, 𝐶} = {𝐶, 𝐴}
212211eleq1i 2835 . . . . . . . 8 ({𝐴, 𝐶} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ 𝐸)
213210, 205, 2123anbi123i 1194 . . . . . . 7 (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
214209, 213bitr3i 268 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
215 df-3an 1109 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸))
216 3anrot 1122 . . . . . . . 8 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))
217 3anrot 1122 . . . . . . . 8 (({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))
218 biid 252 . . . . . . . . 9 ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ 𝐸)
219203, 218, 2123anbi123i 1194 . . . . . . . 8 (({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
220216, 217, 2193bitri 288 . . . . . . 7 (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
221215, 220bitr3i 268 . . . . . 6 ((({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
222208, 214, 2213anbi123i 1194 . . . . 5 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ {𝐵, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
223 df-3an 1109 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
224 anabs1 652 . . . . . 6 (((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
225 anidm 560 . . . . . 6 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
226223, 224, 2253bitri 288 . . . . 5 ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
227199, 222, 2263bitri 288 . . . 4 (((({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸) ∧ ({𝐵, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) ∧ (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐵} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) ∧ (({𝐵, 𝐶} ∈ 𝐸 ∧ {𝐵, 𝐴} ∈ 𝐸) ∧ ({𝐴, 𝐶} ∈ 𝐸 ∧ {𝐴, 𝐵} ∈ 𝐸))) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))
228180, 227syl6bb 278 . . 3 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (((∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐶}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐶}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ 𝐸) ∧ (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐴}} ⊆ 𝐸 ∧ ∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐶}, {𝑥, 𝐵}} ⊆ 𝐸)) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
22913, 98, 2283bitrd 296 . 2 ((((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))
230229ex 401 1 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  ∃!wreu 3057  cdif 3729  wss 3732  {csn 4334  {cpr 4336  {ctp 4338  cfv 6068  Vtxcvtx 26165  Edgcedg 26216  USGraphcusgr 26322   FriendGraph cfrgr 27494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-hash 13322  df-edg 26217  df-umgr 26255  df-usgr 26324  df-frgr 27495
This theorem is referenced by:  3vfriswmgr  27516
  Copyright terms: Public domain W3C validator