Metamath Proof Explorer

Theorem frgr3v

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)

Ref Expression
Hypotheses frgr3v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgr3v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgr3v ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 frgr3v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgr3v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 isfrgr ⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
4 3 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
5 id ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
6 difeq1 ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝑉 ∖ { 𝑘 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) )
7 reueq1 ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
8 6 7 raleqbidv ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
9 5 8 raleqbidv ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
10 9 anbi2d ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
11 10 baibd ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
12 11 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
13 4 12 bitrd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐺 ∈ FriendGraph ↔ ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
14 sneq ⊢ ( 𝑘 = 𝐴 → { 𝑘 } = { 𝐴 } )
15 14 difeq2d ⊢ ( 𝑘 = 𝐴 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) )
16 preq2 ⊢ ( 𝑘 = 𝐴 → { 𝑥 , 𝑘 } = { 𝑥 , 𝐴 } )
17 16 preq1d ⊢ ( 𝑘 = 𝐴 → { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } )
18 17 sseq1d ⊢ ( 𝑘 = 𝐴 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
19 18 reubidv ⊢ ( 𝑘 = 𝐴 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
20 15 19 raleqbidv ⊢ ( 𝑘 = 𝐴 → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
21 sneq ⊢ ( 𝑘 = 𝐵 → { 𝑘 } = { 𝐵 } )
22 21 difeq2d ⊢ ( 𝑘 = 𝐵 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) )
23 preq2 ⊢ ( 𝑘 = 𝐵 → { 𝑥 , 𝑘 } = { 𝑥 , 𝐵 } )
24 23 preq1d ⊢ ( 𝑘 = 𝐵 → { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } )
25 24 sseq1d ⊢ ( 𝑘 = 𝐵 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
26 25 reubidv ⊢ ( 𝑘 = 𝐵 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
27 22 26 raleqbidv ⊢ ( 𝑘 = 𝐵 → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
28 sneq ⊢ ( 𝑘 = 𝐶 → { 𝑘 } = { 𝐶 } )
29 28 difeq2d ⊢ ( 𝑘 = 𝐶 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) )
30 preq2 ⊢ ( 𝑘 = 𝐶 → { 𝑥 , 𝑘 } = { 𝑥 , 𝐶 } )
31 30 preq1d ⊢ ( 𝑘 = 𝐶 → { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } )
32 31 sseq1d ⊢ ( 𝑘 = 𝐶 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
33 32 reubidv ⊢ ( 𝑘 = 𝐶 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
34 29 33 raleqbidv ⊢ ( 𝑘 = 𝐶 → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
35 20 27 34 raltpg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
36 35 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
37 tprot ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
38 37 a1i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 } )
39 38 difeq1d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) = ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) )
40 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
41 40 biimpi ⊢ ( 𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴 )
42 necom ⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
43 42 biimpi ⊢ ( 𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴 )
44 41 43 anim12i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) )
45 44 3adant3 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) )
46 diftpsn3 ⊢ ( ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) → ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
47 45 46 syl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
48 39 47 eqtrd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
49 48 raleqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
50 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
51 50 eqcomi ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 }
52 51 a1i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 } )
53 52 difeq1d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) = ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) )
54 id ⊢ ( 𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵 )
55 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
56 55 biimpi ⊢ ( 𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵 )
57 54 56 anim12ci ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
58 57 3adant2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
59 diftpsn3 ⊢ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
60 58 59 syl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
61 53 60 eqtrd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
62 61 raleqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
63 diftpsn3 ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
64 63 3adant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
65 64 raleqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
66 49 62 65 3anbi123d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
67 66 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
68 preq2 ⊢ ( 𝑙 = 𝐵 → { 𝑥 , 𝑙 } = { 𝑥 , 𝐵 } )
69 68 preq2d ⊢ ( 𝑙 = 𝐵 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } )
70 69 sseq1d ⊢ ( 𝑙 = 𝐵 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
71 70 reubidv ⊢ ( 𝑙 = 𝐵 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
72 preq2 ⊢ ( 𝑙 = 𝐶 → { 𝑥 , 𝑙 } = { 𝑥 , 𝐶 } )
73 72 preq2d ⊢ ( 𝑙 = 𝐶 → { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } )
74 73 sseq1d ⊢ ( 𝑙 = 𝐶 → ( { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
75 74 reubidv ⊢ ( 𝑙 = 𝐶 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
76 71 75 ralprg ⊢ ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ) )
77 76 3adant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ) )
78 72 preq2d ⊢ ( 𝑙 = 𝐶 → { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } )
79 78 sseq1d ⊢ ( 𝑙 = 𝐶 → ( { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
80 79 reubidv ⊢ ( 𝑙 = 𝐶 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
81 preq2 ⊢ ( 𝑙 = 𝐴 → { 𝑥 , 𝑙 } = { 𝑥 , 𝐴 } )
82 81 preq2d ⊢ ( 𝑙 = 𝐴 → { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } )
83 82 sseq1d ⊢ ( 𝑙 = 𝐴 → ( { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
84 83 reubidv ⊢ ( 𝑙 = 𝐴 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
85 80 84 ralprg ⊢ ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ) )
86 85 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ) )
87 86 3adant2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ) )
88 81 preq2d ⊢ ( 𝑙 = 𝐴 → { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } )
89 88 sseq1d ⊢ ( 𝑙 = 𝐴 → ( { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
90 89 reubidv ⊢ ( 𝑙 = 𝐴 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
91 68 preq2d ⊢ ( 𝑙 = 𝐵 → { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } )
92 91 sseq1d ⊢ ( 𝑙 = 𝐵 → ( { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
93 92 reubidv ⊢ ( 𝑙 = 𝐵 → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
94 90 93 ralprg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) )
95 94 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) )
96 77 87 95 3anbi123d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) ) )
97 96 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∀ 𝑙 ∈ { 𝐵 , 𝐶 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐶 , 𝐴 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ∧ ∀ 𝑙 ∈ { 𝐴 , 𝐵 } ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ↔ ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) ) )
98 36 67 97 3bitrd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ∀ 𝑙 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ↔ ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) ) )
99 1 2 frgr3vlem2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) ) )
100 99 imp ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
101 simpll1 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 ∈ 𝑋 )
102 simpll3 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 ∈ 𝑍 )
103 simpll2 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 ∈ 𝑌 )
104 101 102 103 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) )
105 simplr2 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 ≠ 𝐶 )
106 simplr1 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐴 ≠ 𝐵 )
107 58 simpld ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ≠ 𝐵 )
108 107 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 ≠ 𝐵 )
109 105 106 108 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) )
110 tpcomb ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 , 𝐵 }
111 5 110 eqtrdi ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐴 , 𝐶 , 𝐵 } )
112 111 anim1i ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
113 112 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
114 reueq1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 , 𝐵 } → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐶 , 𝐵 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
115 110 114 mp1i ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐴 , 𝐶 , 𝐵 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
116 1 2 frgr3vlem2 ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ) → ( ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐶 , 𝐵 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) )
117 116 imp ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐶 , 𝐵 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
118 115 117 bitrd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐶 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
119 104 109 113 118 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
120 100 119 anbi12d ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ↔ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) )
121 103 102 101 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) )
122 simplr3 ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 ≠ 𝐶 )
123 106 necomd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐵 ≠ 𝐴 )
124 105 necomd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → 𝐶 ≠ 𝐴 )
125 122 123 124 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) )
126 37 eqeq2i ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐵 , 𝐶 , 𝐴 } )
127 126 biimpi ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐵 , 𝐶 , 𝐴 } )
128 127 anim1i ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) )
129 128 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) )
130 reueq1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 } → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐵 , 𝐶 , 𝐴 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
131 37 130 mp1i ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐵 , 𝐶 , 𝐴 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
132 1 2 frgr3vlem2 ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) ) → ( ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐵 , 𝐶 , 𝐴 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) ) )
133 132 imp ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐵 , 𝐶 , 𝐴 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
134 131 133 bitrd ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐶 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
135 121 125 129 134 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
136 103 101 102 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) )
137 123 122 105 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) )
138 tpcoma ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 , 𝐶 }
139 138 eqeq2i ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐵 , 𝐴 , 𝐶 } )
140 139 biimpi ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐵 , 𝐴 , 𝐶 } )
141 140 anim1i ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
142 141 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
143 reueq1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 , 𝐶 } → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐵 , 𝐴 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
144 138 143 mp1i ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐵 , 𝐴 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
145 1 2 frgr3vlem2 ⊢ ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐵 , 𝐴 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) )
146 145 imp ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐵 , 𝐴 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
147 144 146 bitrd ⊢ ( ( ( ( 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐵 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐵 , 𝐴 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
148 136 137 142 147 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
149 135 148 anbi12d ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) )
150 102 101 103 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
151 124 108 106 3jca ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
152 51 eqeq2i ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐶 , 𝐴 , 𝐵 } )
153 152 biimpi ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐶 , 𝐴 , 𝐵 } )
154 153 anim1i ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
155 154 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) )
156 reueq1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 } → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐶 , 𝐴 , 𝐵 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
157 51 156 mp1i ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐶 , 𝐴 , 𝐵 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) )
158 1 2 frgr3vlem2 ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) → ( ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐶 , 𝐴 , 𝐵 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) ) )
159 158 imp ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐶 , 𝐴 , 𝐵 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
160 157 159 bitrd ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐴 , 𝐵 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
161 150 151 155 160 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ↔ ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
162 3anrev ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ↔ ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) )
163 162 biimpi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) )
164 55 42 40 3anbi123i ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
165 164 biimpi ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
166 165 3com13 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
167 163 166 anim12i ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) )
168 tpcoma ⊢ { 𝐵 , 𝐶 , 𝐴 } = { 𝐶 , 𝐵 , 𝐴 }
169 37 168 eqtri ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐵 , 𝐴 }
170 169 eqeq2i ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐶 , 𝐵 , 𝐴 } )
171 170 biimpi ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → 𝑉 = { 𝐶 , 𝐵 , 𝐴 } )
172 171 anim1i ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 = { 𝐶 , 𝐵 , 𝐴 } ∧ 𝐺 ∈ USGraph ) )
173 reueq1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐵 , 𝐴 } → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐶 , 𝐵 , 𝐴 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
174 169 173 mp1i ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐵 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ∃! 𝑥 ∈ { 𝐶 , 𝐵 , 𝐴 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) )
175 1 2 frgr3vlem2 ⊢ ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) → ( ( 𝑉 = { 𝐶 , 𝐵 , 𝐴 } ∧ 𝐺 ∈ USGraph ) → ( ∃! 𝑥 ∈ { 𝐶 , 𝐵 , 𝐴 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ) )
176 175 imp ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐵 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐶 , 𝐵 , 𝐴 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
177 174 176 bitrd ⊢ ( ( ( ( 𝐶 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐶 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) ∧ ( 𝑉 = { 𝐶 , 𝐵 , 𝐴 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
178 167 172 177 syl2an ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) )
179 161 178 anbi12d ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ↔ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ) )
180 120 149 179 3anbi123d ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) ↔ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ∧ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ) ) )
181 prcom ⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 }
182 181 eleq1i ⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐶 , 𝐵 } ∈ 𝐸 )
183 182 anbi2i ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
184 183 anbi2i ⊢ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ↔ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
185 anandir ⊢ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ) )
186 184 185 bitr4i ⊢ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ↔ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
187 prcom ⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
188 187 eleq1i ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐶 } ∈ 𝐸 )
189 188 anbi2i ⊢ ( ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
190 189 anbi2i ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
191 anandir ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )
192 190 191 bitr4i ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
193 prcom ⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
194 193 eleq1i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐵 , 𝐴 } ∈ 𝐸 )
195 194 anbi2i ⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) )
196 195 anbi2i ⊢ ( ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ↔ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
197 anandir ⊢ ( ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
198 196 197 bitr4i ⊢ ( ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ↔ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) )
199 186 192 198 3anbi123i ⊢ ( ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ∧ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ) ↔ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) )
200 3anrot ⊢ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
201 df-3an ⊢ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) )
202 prcom ⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
203 202 eleq1i ⊢ ( { 𝐵 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 )
204 prcom ⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
205 204 eleq1i ⊢ ( { 𝐶 , 𝐵 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ 𝐸 )
206 biid ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐶 , 𝐴 } ∈ 𝐸 )
207 203 205 206 3anbi123i ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
208 200 201 207 3bitr3i ⊢ ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
209 df-3an ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
210 biid ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 )
211 prcom ⊢ { 𝐴 , 𝐶 } = { 𝐶 , 𝐴 }
212 211 eleq1i ⊢ ( { 𝐴 , 𝐶 } ∈ 𝐸 ↔ { 𝐶 , 𝐴 } ∈ 𝐸 )
213 210 205 212 3anbi123i ⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
214 209 213 bitr3i ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
215 df-3an ⊢ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ↔ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) )
216 3anrot ⊢ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
217 3anrot ⊢ ( ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) )
218 biid ⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ 𝐸 )
219 203 218 212 3anbi123i ⊢ ( ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
220 216 217 219 3bitri ⊢ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
221 215 220 bitr3i ⊢ ( ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
222 208 214 221 3anbi123i ⊢ ( ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
223 df-3an ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
224 anabs1 ⊢ ( ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
225 anidm ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
226 223 224 225 3bitri ⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
227 199 222 226 3bitri ⊢ ( ( ( ( { 𝐶 , 𝐴 } ∈ 𝐸 ∧ { 𝐶 , 𝐵 } ∈ 𝐸 ) ∧ ( { 𝐵 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐵 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ∧ ( ( { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐵 , 𝐴 } ∈ 𝐸 ) ∧ ( { 𝐴 , 𝐶 } ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) )
228 180 227 bitrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( ( ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐴 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐵 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ) ∧ ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐴 } } ⊆ 𝐸 ∧ ∃! 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } { { 𝑥 , 𝐶 } , { 𝑥 , 𝐵 } } ⊆ 𝐸 ) ) ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
229 13 98 228 3bitrd ⊢ ( ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) ) → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) )
230 229 ex ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ FriendGraph ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) ) )