Metamath Proof Explorer

Theorem grtriproplem

Description: Lemma for grtriprop . (Contributed by AV, 23-Jul-2025)

Ref Expression
Assertion grtriproplem ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 f1of1 ⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → 𝑓 : ( 0 ..^ 3 ) –1-1→ { 𝑥 , 𝑦 , 𝑧 } )
2 fvf1tp ⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1→ { 𝑥 , 𝑦 , 𝑧 } → ( ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) ) ∨ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) ) ∨ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) ) ) )
3 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 0 ) = 𝑥 )
4 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 1 ) = 𝑦 )
5 3 4 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑥 , 𝑦 } )
6 5 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
7 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 2 ) = 𝑧 )
8 3 7 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑥 , 𝑧 } )
9 8 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
10 4 7 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑦 , 𝑧 } )
11 10 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
12 6 9 11 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
13 12 biimpd ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
14 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 0 ) = 𝑥 )
15 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 1 ) = 𝑧 )
16 14 15 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑥 , 𝑧 } )
17 16 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
18 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 2 ) = 𝑦 )
19 14 18 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑥 , 𝑦 } )
20 19 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
21 15 18 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑧 , 𝑦 } )
22 21 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
23 17 20 22 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) ) )
24 3ancoma ⊢ ( ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
25 prcom ⊢ { 𝑧 , 𝑦 } = { 𝑦 , 𝑧 }
26 25 eleq1i ⊢ ( { 𝑧 , 𝑦 } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 )
27 26 3anbi3i ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
28 24 27 sylbb ⊢ ( ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
29 23 28 biimtrdi ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
30 13 29 jaoi ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
31 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 0 ) = 𝑦 )
32 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 1 ) = 𝑥 )
33 31 32 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑦 , 𝑥 } )
34 33 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
35 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( 𝑓 ‘ 2 ) = 𝑧 )
36 31 35 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑦 , 𝑧 } )
37 36 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
38 32 35 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑥 , 𝑧 } )
39 38 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 ) )
40 34 37 39 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ) )
41 3ancomb ⊢ ( ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
42 prcom ⊢ { 𝑦 , 𝑥 } = { 𝑥 , 𝑦 }
43 42 eleq1i ⊢ ( { 𝑦 , 𝑥 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 )
44 43 3anbi1i ⊢ ( ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
45 41 44 sylbb ⊢ ( ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
46 40 45 biimtrdi ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
47 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 0 ) = 𝑦 )
48 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 1 ) = 𝑧 )
49 47 48 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑦 , 𝑧 } )
50 49 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
51 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 2 ) = 𝑥 )
52 47 51 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑦 , 𝑥 } )
53 52 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
54 48 51 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑧 , 𝑥 } )
55 54 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
56 50 53 55 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) ) )
57 3anrot ⊢ ( ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
58 prcom ⊢ { 𝑧 , 𝑥 } = { 𝑥 , 𝑧 }
59 58 eleq1i ⊢ ( { 𝑧 , 𝑥 } ∈ 𝐸 ↔ { 𝑥 , 𝑧 } ∈ 𝐸 )
60 biid ⊢ ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 )
61 43 59 60 3anbi123i ⊢ ( ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
62 57 61 sylbb ⊢ ( ( { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
63 56 62 biimtrdi ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
64 46 63 jaoi ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑧 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑧 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
65 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 0 ) = 𝑧 )
66 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 1 ) = 𝑥 )
67 65 66 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑧 , 𝑥 } )
68 67 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
69 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( 𝑓 ‘ 2 ) = 𝑦 )
70 65 69 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑧 , 𝑦 } )
71 70 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
72 66 69 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑥 , 𝑦 } )
73 72 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
74 68 71 73 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ) )
75 3anrot ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
76 prcom ⊢ { 𝑥 , 𝑧 } = { 𝑧 , 𝑥 }
77 76 eleq1i ⊢ ( { 𝑥 , 𝑧 } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 )
78 prcom ⊢ { 𝑦 , 𝑧 } = { 𝑧 , 𝑦 }
79 78 eleq1i ⊢ ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 )
80 biid ⊢ ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 )
81 77 79 80 3anbi123i ⊢ ( ( { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
82 75 81 sylbbr ⊢ ( ( { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
83 74 82 biimtrdi ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
84 simp1 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 0 ) = 𝑧 )
85 simp2 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 1 ) = 𝑦 )
86 84 85 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } = { 𝑧 , 𝑦 } )
87 86 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
88 simp3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( 𝑓 ‘ 2 ) = 𝑥 )
89 84 88 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } = { 𝑧 , 𝑥 } )
90 89 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑧 , 𝑥 } ∈ 𝐸 ) )
91 85 88 preq12d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } = { 𝑦 , 𝑥 } )
92 91 eleq1d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
93 87 90 92 3anbi123d ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ↔ ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
94 3anrev ⊢ ( ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ↔ ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) )
95 43 59 26 3anbi123i ⊢ ( ( { 𝑦 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑧 , 𝑦 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
96 94 95 sylbb ⊢ ( ( { 𝑧 , 𝑦 } ∈ 𝐸 ∧ { 𝑧 , 𝑥 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
97 93 96 biimtrdi ⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
98 83 97 jaoi ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( 𝑓 ‘ 2 ) = 𝑦 ) ∨ ( ( 𝑓 ‘ 0 ) = 𝑧 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( 𝑓 ‘ 2 ) = 𝑥 ) ) → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
99 30 64 98 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 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
100 1 2 99 3syl ⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
101 100 imp ⊢ ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ { 𝑥 , 𝑦 , 𝑧 } ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )