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

Metamath Proof Explorer

Theorem isgrtri

Description: A triangle in a graph. (Contributed by AV, 20-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 grtriprop ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
4 df-tp ⊢ { 𝑥 , 𝑦 , 𝑧 } = ( { 𝑥 , 𝑦 } ∪ { 𝑧 } )
5 prelpwi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 )
6 snelpwi ⊢ ( 𝑧 ∈ 𝑉 → { 𝑧 } ∈ 𝒫 𝑉 )
7 5 6 anim12i ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑉 ) → ( { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 ∧ { 𝑧 } ∈ 𝒫 𝑉 ) )
8 7 anasss ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 ∧ { 𝑧 } ∈ 𝒫 𝑉 ) )
9 pwuncl ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 ∧ { 𝑧 } ∈ 𝒫 𝑉 ) → ( { 𝑥 , 𝑦 } ∪ { 𝑧 } ) ∈ 𝒫 𝑉 )
10 8 9 syl ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∪ { 𝑧 } ) ∈ 𝒫 𝑉 )
11 4 10 eqeltrid ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { 𝑥 , 𝑦 , 𝑧 } ∈ 𝒫 𝑉 )
12 11 adantr ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → { 𝑥 , 𝑦 , 𝑧 } ∈ 𝒫 𝑉 )
13 eleq1 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( 𝑇 ∈ 𝒫 𝑉 ↔ { 𝑥 , 𝑦 , 𝑧 } ∈ 𝒫 𝑉 ) )
14 13 3ad2ant1 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝑇 ∈ 𝒫 𝑉 ↔ { 𝑥 , 𝑦 , 𝑧 } ∈ 𝒫 𝑉 ) )
15 14 adantl ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑇 ∈ 𝒫 𝑉 ↔ { 𝑥 , 𝑦 , 𝑧 } ∈ 𝒫 𝑉 ) )
16 12 15 mpbird ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → 𝑇 ∈ 𝒫 𝑉 )
17 ovex ⊢ ( 0 ..^ 3 ) ∈ V
18 17 mptex ⊢ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ∈ V
19 18 a1i ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ∈ V )
20 3anass ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) )
21 20 biimpri ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) )
22 fveq2 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ♯ ‘ 𝑇 ) = ( ♯ ‘ { 𝑥 , 𝑦 , 𝑧 } ) )
23 22 eqcomd ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ♯ ‘ { 𝑥 , 𝑦 , 𝑧 } ) = ( ♯ ‘ 𝑇 ) )
24 23 3ad2ant1 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( ♯ ‘ { 𝑥 , 𝑦 , 𝑧 } ) = ( ♯ ‘ 𝑇 ) )
25 simp2 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( ♯ ‘ 𝑇 ) = 3 )
26 24 25 eqtrd ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( ♯ ‘ { 𝑥 , 𝑦 , 𝑧 } ) = 3 )
27 eqid ⊢ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) )
28 eqid ⊢ { 𝑥 , 𝑦 , 𝑧 } = { 𝑥 , 𝑦 , 𝑧 }
29 27 28 tpf1o ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ ( ♯ ‘ { 𝑥 , 𝑦 , 𝑧 } ) = 3 ) → ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } )
30 21 26 29 syl2an ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } )
31 f1oeq3 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
32 31 3ad2ant1 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
33 32 adantl ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
34 30 33 mpbird ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
35 27 tpf1ofv0 ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) = 𝑥 )
36 35 adantr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) = 𝑥 )
37 27 tpf1ofv1 ⊢ ( 𝑦 ∈ 𝑉 → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) = 𝑦 )
38 37 adantr ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) = 𝑦 )
39 38 adantl ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) = 𝑦 )
40 36 39 preq12d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } = { 𝑥 , 𝑦 } )
41 40 eqcomd ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { 𝑥 , 𝑦 } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } )
42 41 eleq1d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ) )
43 27 tpf1ofv2 ⊢ ( 𝑧 ∈ 𝑉 → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) = 𝑧 )
44 43 adantl ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) = 𝑧 )
45 44 adantl ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) = 𝑧 )
46 36 45 preq12d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } = { 𝑥 , 𝑧 } )
47 46 eqcomd ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { 𝑥 , 𝑧 } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } )
48 47 eleq1d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑧 } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) )
49 39 45 preq12d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } = { 𝑦 , 𝑧 } )
50 49 eqcomd ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → { 𝑦 , 𝑧 } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } )
51 50 eleq1d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) )
52 42 48 51 3anbi123d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) )
53 52 biimpd ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) )
54 53 2a1d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) ) ) )
55 54 3imp2 ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) )
56 34 55 jca ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) )
57 f1oeq1 ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) )
58 fveq1 ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) )
59 fveq1 ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( 𝑓 ‘ 1 ) = ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) )
60 58 59 preq12d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } )
61 60 eleq1d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ) )
62 fveq1 ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( 𝑓 ‘ 2 ) = ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) )
63 58 62 preq12d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } )
64 63 eleq1d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) )
65 59 62 preq12d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } )
66 65 eleq1d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) )
67 61 64 66 3anbi123d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) )
68 57 67 anbi12d ⊢ ( 𝑓 = ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) → ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ↔ ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 0 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ∧ { ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 1 ) , ( ( 𝑖 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑖 = 0 , 𝑥 , if ( 𝑖 = 1 , 𝑦 , 𝑧 ) ) ) ‘ 2 ) } ∈ 𝐸 ) ) ) )
69 19 56 68 spcedv ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) )
70 16 69 jca ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
71 1 1vgrex ⊢ ( 𝑥 ∈ 𝑉 → 𝐺 ∈ V )
72 1 2 grtri ⊢ ( 𝐺 ∈ V → ( GrTriangles ‘ 𝐺 ) = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )
73 72 eleq2d ⊢ ( 𝐺 ∈ V → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ 𝑇 ∈ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ) )
74 71 73 syl ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ 𝑇 ∈ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ) )
75 f1oeq3 ⊢ ( 𝑡 = 𝑇 → ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ↔ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) )
76 75 anbi1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ↔ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
77 76 exbidv ⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
78 77 elrab ⊢ ( 𝑇 ∈ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
79 74 78 bitrdi ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) ) )
80 79 adantr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) ) )
81 80 adantr ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ( 𝑇 ∈ 𝒫 𝑉 ∧ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) ) )
82 70 81 mpbird ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
83 82 ex ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ) )
84 83 rexlimdvva ⊢ ( 𝑥 ∈ 𝑉 → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ) )
85 84 rexlimiv ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
86 3 85 impbii ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )