This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grtriprop

Description: The properties of a triangle. (Contributed by AV, 25-Jul-2025)

Ref Expression
Hypotheses grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion grtriprop ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 elfvex ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → 𝐺 ∈ V )
4 1 2 grtri ⊢ ( 𝐺 ∈ V → ( GrTriangles ‘ 𝐺 ) = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )
5 3 4 syl ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ( GrTriangles ‘ 𝐺 ) = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )
6 5 eleq2d ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ 𝑇 ∈ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ) )
7 f1oeq3 ⊢ ( 𝑡 = 𝑇 → ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ↔ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) )
8 7 anbi1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ↔ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
9 8 exbidv ⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
10 9 elrab ⊢ ( 𝑇 ∈ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
11 6 10 bitrdi ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) ) )
12 ovexd ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( 0 ..^ 3 ) ∈ V )
13 simpr ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
14 12 13 hasheqf1od ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) )
15 eqcom ⊢ ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
16 3nn0 ⊢ 3 ∈ ℕ0
17 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
18 16 17 mp1i ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
19 18 eqeq2d ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) ↔ ( ♯ ‘ 𝑇 ) = 3 ) )
20 15 19 bitrid ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( ♯ ‘ 𝑇 ) = 3 ) )
21 hash3tpb ⊢ ( 𝑇 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑇 ) = 3 ↔ ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
22 21 adantr ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ 𝑇 ) = 3 ↔ ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
23 22 biimpa ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) )
24 elpwi ⊢ ( 𝑇 ∈ 𝒫 𝑉 → 𝑇 ⊆ 𝑉 )
25 ss2rexv ⊢ ( 𝑇 ⊆ 𝑉 → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
26 ssrexv ⊢ ( 𝑇 ⊆ 𝑉 → ( ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
27 26 reximdv ⊢ ( 𝑇 ⊆ 𝑉 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
28 27 reximdv ⊢ ( 𝑇 ⊆ 𝑉 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
29 25 28 syld ⊢ ( 𝑇 ⊆ 𝑉 → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
30 24 29 syl ⊢ ( 𝑇 ∈ 𝒫 𝑉 → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
31 30 adantr ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
32 31 adantr ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) )
33 simprr ⊢ ( ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) → 𝑇 = { 𝑥 , 𝑦 , 𝑧 } )
34 simp-5r ⊢ ( ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) → ( ♯ ‘ 𝑇 ) = 3 )
35 f1oeq3 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
36 grtriproplem ⊢ ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
37 36 2a1d ⊢ ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
38 37 ex ⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
39 38 a1d ⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) ) )
40 35 39 biimtrdi ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) ) ) )
41 40 adantld ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) ) ) )
42 41 imp4c ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑉 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
43 42 imp4c ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
44 43 adantl ⊢ ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
45 44 impcom ⊢ ( ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
46 33 34 45 3jca ⊢ ( ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) ) → ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
47 46 ex ⊢ ( ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝑉 ) → ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
48 47 reximdva ⊢ ( ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
49 48 reximdvva ⊢ ( ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
50 49 ex ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
51 50 com23 ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
52 32 51 syld ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑇 ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
53 23 52 mpd ⊢ ( ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
54 53 ex ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
55 20 54 sylbid ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
56 14 55 mpd ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
57 56 expimpd ⊢ ( 𝑇 ∈ 𝒫 𝑉 → ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
58 57 exlimdv ⊢ ( 𝑇 ∈ 𝒫 𝑉 → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
59 58 imp ⊢ ( ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
60 11 59 biimtrdi ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
61 60 pm2.43i ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )