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

Metamath Proof Explorer

Theorem grtriproplem

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

Ref Expression
Assertion grtriproplem 
|- ( ( f : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) )

Proof

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