NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  transex GIF version

Theorem transex 5910
Description: The class of all transitive relationships is a set. (Contributed by SF, 19-Feb-2015.)
Assertion
Ref Expression
transex Trans V

Proof of Theorem transex
Dummy variables a q r x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trans 5899 . . 3 Trans = {r, a x a y a z a ((xry yrz) → xrz)}
2 vex 2862 . . . . . . 7 r V
3 vex 2862 . . . . . . 7 a V
42, 3opex 4588 . . . . . 6 r, a V
54elcompl 3225 . . . . 5 (r, a ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) ↔ ¬ r, a (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c))
6 elin 3219 . . . . . . . . . 10 ({x}, r, a ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) ↔ ({x}, r, a Ins2 S {x}, r, a (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)))
72otelins2 5791 . . . . . . . . . . . 12 ({x}, r, a Ins2 S {x}, a S )
8 vex 2862 . . . . . . . . . . . . 13 x V
98, 3opelssetsn 4760 . . . . . . . . . . . 12 ({x}, a S x a)
107, 9bitri 240 . . . . . . . . . . 11 ({x}, r, a Ins2 S x a)
11 elima1c 4947 . . . . . . . . . . . 12 ({x}, r, a (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c) ↔ y{y}, {x}, r, a ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)))
12 elin 3219 . . . . . . . . . . . . . 14 ({y}, {x}, r, a ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) ↔ ({y}, {x}, r, a Ins2 Ins2 S {y}, {x}, r, a (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)))
13 snex 4111 . . . . . . . . . . . . . . . . 17 {x} V
1413otelins2 5791 . . . . . . . . . . . . . . . 16 ({y}, {x}, r, a Ins2 Ins2 S {y}, r, a Ins2 S )
152otelins2 5791 . . . . . . . . . . . . . . . 16 ({y}, r, a Ins2 S {y}, a S )
16 vex 2862 . . . . . . . . . . . . . . . . 17 y V
1716, 3opelssetsn 4760 . . . . . . . . . . . . . . . 16 ({y}, a S y a)
1814, 15, 173bitri 262 . . . . . . . . . . . . . . 15 ({y}, {x}, r, a Ins2 Ins2 S y a)
19 elima1c 4947 . . . . . . . . . . . . . . . 16 ({y}, {x}, r, a (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c) ↔ z{z}, {y}, {x}, r, a ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))))
20 elin 3219 . . . . . . . . . . . . . . . . . 18 ({z}, {y}, {x}, r, a ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ ({z}, {y}, {x}, r, a Ins2 Ins2 Ins2 S {z}, {y}, {x}, r, a (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))))
21 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {y} V
2221otelins2 5791 . . . . . . . . . . . . . . . . . . . 20 ({z}, {y}, {x}, r, a Ins2 Ins2 Ins2 S {z}, {x}, r, a Ins2 Ins2 S )
2313otelins2 5791 . . . . . . . . . . . . . . . . . . . 20 ({z}, {x}, r, a Ins2 Ins2 S {z}, r, a Ins2 S )
242otelins2 5791 . . . . . . . . . . . . . . . . . . . . 21 ({z}, r, a Ins2 S {z}, a S )
25 vex 2862 . . . . . . . . . . . . . . . . . . . . . 22 z V
2625, 3opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . 21 ({z}, a S z a)
2724, 26bitri 240 . . . . . . . . . . . . . . . . . . . 20 ({z}, r, a Ins2 S z a)
2822, 23, 273bitri 262 . . . . . . . . . . . . . . . . . . 19 ({z}, {y}, {x}, r, a Ins2 Ins2 Ins2 S z a)
29 eldif 3221 . . . . . . . . . . . . . . . . . . . 20 ({z}, {y}, {x}, r, a (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ({z}, {y}, {x}, r, a ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ¬ {z}, {y}, {x}, r, a Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)))
30 elin 3219 . . . . . . . . . . . . . . . . . . . . . 22 ({z}, {y}, {x}, r, a ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ↔ ({z}, {y}, {x}, r, a (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) {z}, {y}, {x}, r, a (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)))
31 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25 {z} V
32 opelxp 4811 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({z}, {y}, {x}, r, a (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ({z} V {y}, {x}, r, a Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)))
3331, 32mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . 24 ({z}, {y}, {x}, r, a (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ {y}, {x}, r, a Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))
343oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, {x}, r, a Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ {y}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))
35 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({z}, {y}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ ({z}, {y}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) {z}, {y}, {x}, r Ins2 Ins2 S ))
362oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({z}, {y}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) ↔ {z}, {y}, {x} SI3 (2nd ⊗ 1st ))
3725, 16, 8otsnelsi3 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({z}, {y}, {x} SI3 (2nd ⊗ 1st ) ↔ z, y, x (2nd ⊗ 1st ))
38 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (z, y, x (2nd ⊗ 1st ) ↔ (z, y 2nd z, x 1st ))
39 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((z, y 2nd z, x 1st ) ↔ (z, x 1st z, y 2nd ))
40 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (z1st xz, x 1st )
41 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (z2nd yz, y 2nd )
4240, 41anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((z1st x z2nd y) ↔ (z, x 1st z, y 2nd ))
4339, 42bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((z, y 2nd z, x 1st ) ↔ (z1st x z2nd y))
448, 16op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((z1st x z2nd y) ↔ z = x, y)
4538, 43, 443bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (z, y, x (2nd ⊗ 1st ) ↔ z = x, y)
4636, 37, 453bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({z}, {y}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) ↔ z = x, y)
4721otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({z}, {y}, {x}, r Ins2 Ins2 S {z}, {x}, r Ins2 S )
4813otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({z}, {x}, r Ins2 S {z}, r S )
4925, 2opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({z}, r S z r)
5047, 48, 493bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({z}, {y}, {x}, r Ins2 Ins2 S z r)
5146, 50anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({z}, {y}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) {z}, {y}, {x}, r Ins2 Ins2 S ) ↔ (z = x, y z r))
5235, 51bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({z}, {y}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ (z = x, y z r))
5352exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (z{z}, {y}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ z(z = x, y z r))
54 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({y}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ z{z}, {y}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ))
55 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (xryx, y r)
56 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x, y rz(z = x, y z r))
5755, 56bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (xryz(z = x, y z r))
5853, 54, 573bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xry)
5933, 34, 583bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 ({z}, {y}, {x}, r, a (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ xry)
60 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({q}, {z}, {y}, {x}, r, a ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ ({q}, {z}, {y}, {x}, r, a Ins4 SI3 (2nd ⊗ 1st ) {q}, {z}, {y}, {x}, r, a Ins2 Ins2 Ins2 Ins3 S ))
6113, 4opex 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {x}, r, a V
6261oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q}, {z}, {y}, {x}, r, a Ins4 SI3 (2nd ⊗ 1st ) ↔ {q}, {z}, {y} SI3 (2nd ⊗ 1st ))
63 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 q V
6463, 25, 16otsnelsi3 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q}, {z}, {y} SI3 (2nd ⊗ 1st ) ↔ q, z, y (2nd ⊗ 1st ))
65 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (q, z, y (2nd ⊗ 1st ) ↔ (q, z 2nd q, y 1st ))
66 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((q, z 2nd q, y 1st ) ↔ (q, y 1st q, z 2nd ))
67 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (q1st yq, y 1st )
68 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (q2nd zq, z 2nd )
6967, 68anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((q1st y q2nd z) ↔ (q, y 1st q, z 2nd ))
7066, 69bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((q, z 2nd q, y 1st ) ↔ (q1st y q2nd z))
7116, 25op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((q1st y q2nd z) ↔ q = y, z)
7265, 70, 713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (q, z, y (2nd ⊗ 1st ) ↔ q = y, z)
7362, 64, 723bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({q}, {z}, {y}, {x}, r, a Ins4 SI3 (2nd ⊗ 1st ) ↔ q = y, z)
7431otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q}, {z}, {y}, {x}, r, a Ins2 Ins2 Ins2 Ins3 S {q}, {y}, {x}, r, a Ins2 Ins2 Ins3 S )
7521otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q}, {y}, {x}, r, a Ins2 Ins2 Ins3 S {q}, {x}, r, a Ins2 Ins3 S )
7613otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({q}, {x}, r, a Ins2 Ins3 S {q}, r, a Ins3 S )
773otelins3 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({q}, r, a Ins3 S {q}, r S )
7863, 2opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({q}, r S q r)
7976, 77, 783bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({q}, {x}, r, a Ins2 Ins3 S q r)
8074, 75, 793bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({q}, {z}, {y}, {x}, r, a Ins2 Ins2 Ins2 Ins3 S q r)
8173, 80anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({q}, {z}, {y}, {x}, r, a Ins4 SI3 (2nd ⊗ 1st ) {q}, {z}, {y}, {x}, r, a Ins2 Ins2 Ins2 Ins3 S ) ↔ (q = y, z q r))
8260, 81bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({q}, {z}, {y}, {x}, r, a ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ (q = y, z q r))
8382exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (q{q}, {z}, {y}, {x}, r, a ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ q(q = y, z q r))
84 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . . 24 ({z}, {y}, {x}, r, a (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ↔ q{q}, {z}, {y}, {x}, r, a ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ))
85 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . 25 (yrzy, z r)
86 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . 25 (y, z rq(q = y, z q r))
8785, 86bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (yrzq(q = y, z q r))
8883, 84, 873bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . 23 ({z}, {y}, {x}, r, a (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ↔ yrz)
8959, 88anbi12i 678 . . . . . . . . . . . . . . . . . . . . . 22 (({z}, {y}, {x}, r, a (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) {z}, {y}, {x}, r, a (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ↔ (xry yrz))
9030, 89bitri 240 . . . . . . . . . . . . . . . . . . . . 21 ({z}, {y}, {x}, r, a ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ↔ (xry yrz))
9121otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . 23 ({z}, {y}, {x}, r, a Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ {z}, {x}, r, a Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))
923oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . 23 ({z}, {x}, r, a Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ {z}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))
93 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({y}, {z}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ ({y}, {z}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) {y}, {z}, {x}, r Ins2 Ins2 S ))
942oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y}, {z}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) ↔ {y}, {z}, {x} SI3 (2nd ⊗ 1st ))
9516, 25, 8otsnelsi3 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({y}, {z}, {x} SI3 (2nd ⊗ 1st ) ↔ y, z, x (2nd ⊗ 1st ))
96 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((y, z 2nd y, x 1st ) ↔ (y, x 1st y, z 2nd ))
97 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (y, z, x (2nd ⊗ 1st ) ↔ (y, z 2nd y, x 1st ))
98 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (y1st xy, x 1st )
99 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (y2nd zy, z 2nd )
10098, 99anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((y1st x y2nd z) ↔ (y, x 1st y, z 2nd ))
10196, 97, 1003bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (y, z, x (2nd ⊗ 1st ) ↔ (y1st x y2nd z))
1028, 25op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((y1st x y2nd z) ↔ y = x, z)
10395, 101, 1023bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y}, {z}, {x} SI3 (2nd ⊗ 1st ) ↔ y = x, z)
10494, 103bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({y}, {z}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) ↔ y = x, z)
10531otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y}, {z}, {x}, r Ins2 Ins2 S {y}, {x}, r Ins2 S )
10613otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y}, {x}, r Ins2 S {y}, r S )
10716, 2opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y}, r S y r)
108105, 106, 1073bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({y}, {z}, {x}, r Ins2 Ins2 S y r)
109104, 108anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (({y}, {z}, {x}, r Ins4 SI3 (2nd ⊗ 1st ) {y}, {z}, {x}, r Ins2 Ins2 S ) ↔ (y = x, z y r))
11093, 109bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({y}, {z}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ (y = x, z y r))
111110exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (y{y}, {z}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ y(y = x, z y r))
112 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . . 24 ({z}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ y{y}, {z}, {x}, r ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ))
113 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . 25 (xrzx, z r)
114 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x, z ry(y = x, z y r))
115113, 114bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (xrzy(y = x, z y r))
116111, 112, 1153bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . 23 ({z}, {x}, r (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz)
11791, 92, 1163bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 ({z}, {y}, {x}, r, a Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz)
118117notbii 287 . . . . . . . . . . . . . . . . . . . . 21 {z}, {y}, {x}, r, a Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ ¬ xrz)
11990, 118anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 (({z}, {y}, {x}, r, a ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ¬ {z}, {y}, {x}, r, a Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ((xry yrz) ¬ xrz))
12029, 119bitri 240 . . . . . . . . . . . . . . . . . . 19 ({z}, {y}, {x}, r, a (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ((xry yrz) ¬ xrz))
12128, 120anbi12i 678 . . . . . . . . . . . . . . . . . 18 (({z}, {y}, {x}, r, a Ins2 Ins2 Ins2 S {z}, {y}, {x}, r, a (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ (z a ((xry yrz) ¬ xrz)))
12220, 121bitri 240 . . . . . . . . . . . . . . . . 17 ({z}, {y}, {x}, r, a ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ (z a ((xry yrz) ¬ xrz)))
123122exbii 1582 . . . . . . . . . . . . . . . 16 (z{z}, {y}, {x}, r, a ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ z(z a ((xry yrz) ¬ xrz)))
124 df-rex 2620 . . . . . . . . . . . . . . . . 17 (z a ((xry yrz) ¬ xrz) ↔ z(z a ((xry yrz) ¬ xrz)))
125 rexanali 2660 . . . . . . . . . . . . . . . . 17 (z a ((xry yrz) ¬ xrz) ↔ ¬ z a ((xry yrz) → xrz))
126124, 125bitr3i 242 . . . . . . . . . . . . . . . 16 (z(z a ((xry yrz) ¬ xrz)) ↔ ¬ z a ((xry yrz) → xrz))
12719, 123, 1263bitri 262 . . . . . . . . . . . . . . 15 ({y}, {x}, r, a (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c) ↔ ¬ z a ((xry yrz) → xrz))
12818, 127anbi12i 678 . . . . . . . . . . . . . 14 (({y}, {x}, r, a Ins2 Ins2 S {y}, {x}, r, a (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) ↔ (y a ¬ z a ((xry yrz) → xrz)))
12912, 128bitri 240 . . . . . . . . . . . . 13 ({y}, {x}, r, a ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) ↔ (y a ¬ z a ((xry yrz) → xrz)))
130129exbii 1582 . . . . . . . . . . . 12 (y{y}, {x}, r, a ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) ↔ y(y a ¬ z a ((xry yrz) → xrz)))
131 df-rex 2620 . . . . . . . . . . . . 13 (y a ¬ z a ((xry yrz) → xrz) ↔ y(y a ¬ z a ((xry yrz) → xrz)))
132 rexnal 2625 . . . . . . . . . . . . 13 (y a ¬ z a ((xry yrz) → xrz) ↔ ¬ y a z a ((xry yrz) → xrz))
133131, 132bitr3i 242 . . . . . . . . . . . 12 (y(y a ¬ z a ((xry yrz) → xrz)) ↔ ¬ y a z a ((xry yrz) → xrz))
13411, 130, 1333bitri 262 . . . . . . . . . . 11 ({x}, r, a (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c) ↔ ¬ y a z a ((xry yrz) → xrz))
13510, 134anbi12i 678 . . . . . . . . . 10 (({x}, r, a Ins2 S {x}, r, a (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) ↔ (x a ¬ y a z a ((xry yrz) → xrz)))
1366, 135bitri 240 . . . . . . . . 9 ({x}, r, a ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) ↔ (x a ¬ y a z a ((xry yrz) → xrz)))
137136exbii 1582 . . . . . . . 8 (x{x}, r, a ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) ↔ x(x a ¬ y a z a ((xry yrz) → xrz)))
138 elima1c 4947 . . . . . . . 8 (r, a (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) ↔ x{x}, r, a ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)))
139 df-rex 2620 . . . . . . . 8 (x a ¬ y a z a ((xry yrz) → xrz) ↔ x(x a ¬ y a z a ((xry yrz) → xrz)))
140137, 138, 1393bitr4i 268 . . . . . . 7 (r, a (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) ↔ x a ¬ y a z a ((xry yrz) → xrz))
141 rexnal 2625 . . . . . . 7 (x a ¬ y a z a ((xry yrz) → xrz) ↔ ¬ x a y a z a ((xry yrz) → xrz))
142140, 141bitri 240 . . . . . 6 (r, a (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) ↔ ¬ x a y a z a ((xry yrz) → xrz))
143142con2bii 322 . . . . 5 (x a y a z a ((xry yrz) → xrz) ↔ ¬ r, a (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c))
1445, 143bitr4i 243 . . . 4 (r, a ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) ↔ x a y a z a ((xry yrz) → xrz))
145144opabbi2i 4866 . . 3 ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) = {r, a x a y a z a ((xry yrz) → xrz)}
1461, 145eqtr4i 2376 . 2 Trans = ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c)
147 ssetex 4744 . . . . . 6 S V
148147ins2ex 5797 . . . . 5 Ins2 S V
149148ins2ex 5797 . . . . . . 7 Ins2 Ins2 S V
150149ins2ex 5797 . . . . . . . . 9 Ins2 Ins2 Ins2 S V
151 vvex 4109 . . . . . . . . . . . 12 V V
152 2ndex 5112 . . . . . . . . . . . . . . . . . 18 2nd V
153 1stex 4739 . . . . . . . . . . . . . . . . . 18 1st V
154152, 153txpex 5785 . . . . . . . . . . . . . . . . 17 (2nd ⊗ 1st ) V
155154si3ex 5806 . . . . . . . . . . . . . . . 16 SI3 (2nd ⊗ 1st ) V
156155ins4ex 5799 . . . . . . . . . . . . . . 15 Ins4 SI3 (2nd ⊗ 1st ) V
157156, 149inex 4105 . . . . . . . . . . . . . 14 ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) V
158 1cex 4142 . . . . . . . . . . . . . 14 1c V
159157, 158imaex 4747 . . . . . . . . . . . . 13 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) V
160159ins4ex 5799 . . . . . . . . . . . 12 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) V
161151, 160xpex 5115 . . . . . . . . . . 11 (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) V
162147ins3ex 5798 . . . . . . . . . . . . . . . 16 Ins3 S V
163162ins2ex 5797 . . . . . . . . . . . . . . 15 Ins2 Ins3 S V
164163ins2ex 5797 . . . . . . . . . . . . . 14 Ins2 Ins2 Ins3 S V
165164ins2ex 5797 . . . . . . . . . . . . 13 Ins2 Ins2 Ins2 Ins3 S V
166156, 165inex 4105 . . . . . . . . . . . 12 ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) V
167166, 158imaex 4747 . . . . . . . . . . 11 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) V
168161, 167inex 4105 . . . . . . . . . 10 ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) V
169160ins2ex 5797 . . . . . . . . . 10 Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) V
170168, 169difex 4107 . . . . . . . . 9 (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) V
171150, 170inex 4105 . . . . . . . 8 ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) V
172171, 158imaex 4747 . . . . . . 7 (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c) V
173149, 172inex 4105 . . . . . 6 ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) V
174173, 158imaex 4747 . . . . 5 (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c) V
175148, 174inex 4105 . . . 4 ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) V
176175, 158imaex 4747 . . 3 (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) V
177176complex 4104 . 2 ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “ 1c)) “ 1c)) “ 1c) V
178146, 177eqeltri 2423 1 Trans V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wa 358  wex 1541   = wceq 1642   wcel 1710  wral 2614  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cin 3208  {csn 3737  1cc1c 4134  cop 4561  {copab 4622   class class class wbr 4639  1st c1st 4717   S csset 4719  cima 4722   × cxp 4770  2nd c2nd 4783  ctxp 5735   Ins2 cins2 5749   Ins3 cins3 5751   Ins4 cins4 5755   SI3 csi3 5757   Trans ctrans 5888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-xp 4784  df-cnv 4785  df-2nd 4797  df-txp 5736  df-ins2 5750  df-ins3 5752  df-ins4 5756  df-si3 5758  df-trans 5899
This theorem is referenced by:  partialex  5917  erex  5920
  Copyright terms: Public domain W3C validator