Metamath Proof Explorer

Theorem grtrif1o

Description: Any bijection onto a triangle preserves the edges of the triangle. (Contributed by AV, 25-Jul-2025)

Ref Expression
Hypotheses grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion grtrif1o ( ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ∧ 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 grtriprop ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
4 f1oeq3 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
5 4 adantr ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ↔ 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ) )
6 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑥 , 𝑦 } )
7 6 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
8 7 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
9 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑥 , 𝑧 } )
10 9 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
11 10 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
12 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑦 , 𝑧 } )
13 12 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
14 13 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
15 8 11 14 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
16 15 biimprd ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
17 3ancoma ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
18 prcom ⊢ { 𝑦 , 𝑧 } = { 𝑧 , 𝑦 }
19 18 eleq1i ⊢ ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 )
20 19 3anbi3i ⊢ ( ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
21 17 20 sylbb ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
22 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑥 , 𝑧 } )
23 22 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
24 23 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
25 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑥 , 𝑦 } )
26 25 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
27 26 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
28 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑧 , 𝑦 } )
29 28 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
30 29 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
31 24 27 30 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) ) )
32 21 31 imbitrrid ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
33 16 32 jaoi ⊢ ( ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
34 3ancomb ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
35 prcom ⊢ { 𝑥 , 𝑦 } = { 𝑦 , 𝑥 }
36 35 eleq1i ⊢ ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 )
37 36 3anbi1i ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
38 34 37 sylbb ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
39 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑦 , 𝑥 } )
40 39 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
41 40 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
42 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑦 , 𝑧 } )
43 42 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
44 43 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
45 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑥 , 𝑧 } )
46 45 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
47 46 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
48 41 44 47 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ) )
49 38 48 imbitrrid ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
50 3anrot ⊢ ( ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
51 biid ⊢ ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 )
52 prcom ⊢ { 𝑥 , 𝑧 } = { 𝑧 , 𝑥 }
53 52 eleq1i ⊢ ( { 𝑥 , 𝑧 } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 )
54 51 36 53 3anbi123i ⊢ ( ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
55 50 54 sylbb1 ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
56 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑦 , 𝑧 } )
57 56 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
58 57 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
59 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑦 , 𝑥 } )
60 59 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
61 60 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
62 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑧 , 𝑥 } )
63 62 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
64 63 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
65 58 61 64 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) ) )
66 55 65 imbitrrid ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
67 49 66 jaoi ⊢ ( ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
68 3anrot ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
69 biid ⊢ ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 )
70 53 19 69 3anbi123i ⊢ ( ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
71 68 70 sylbb ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
72 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑧 , 𝑥 } )
73 72 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
74 73 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
75 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑧 , 𝑦 } )
76 75 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
77 76 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
78 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑥 , 𝑦 } )
79 78 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
80 79 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
81 74 77 80 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
82 71 81 imbitrrid ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
83 3anrev ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
84 19 53 36 3anbi123i ⊢ ( ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
85 83 84 sylbb ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
86 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } = { 𝑧 , 𝑦 } )
87 86 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
88 87 3adant3 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
89 preq12 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } = { 𝑧 , 𝑥 } )
90 89 eleq1d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
91 90 3adant2 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
92 preq12 ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } = { 𝑦 , 𝑥 } )
93 92 eleq1d ⊢ ( ( ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
94 93 3adant1 ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
95 88 91 94 3anbi123d ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
96 85 95 imbitrrid ⊢ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
97 82 96 jaoi ⊢ ( ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
98 33 67 97 3jaoi ⊢ ( ( ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
99 f1of1 ⊢ ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → 𝐹 : ( 0 ..^ 3 ) –1-1→ { 𝑥 , 𝑦 , 𝑧 } )
100 fvf1tp ⊢ ( 𝐹 : ( 0 ..^ 3 ) –1-1→ { 𝑥 , 𝑦 , 𝑧 } → ( ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ) )
101 99 100 syl ⊢ ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( ( ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑥 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑦 ∧ ( 𝐹 ‘ 1 ) = 𝑧 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ∨ ( ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑥 ∧ ( 𝐹 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝐹 ‘ 0 ) = 𝑧 ∧ ( 𝐹 ‘ 1 ) = 𝑦 ∧ ( 𝐹 ‘ 2 ) = 𝑥 ) ) ) )
102 98 101 syl11 ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
103 102 adantl ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
104 5 103 sylbid ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
105 104 3adant2 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
106 105 a1i ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) ) )
107 106 rexlimivv ⊢ ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
108 107 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
109 3 108 syl ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ( 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) ) )
110 109 imp ⊢ ( ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ∧ 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 1 ) , ( 𝐹 ‘ 2 ) } ∈ 𝐸 ) )