transex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > transex		Unicode 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

Proof of Theorem transex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-trans 5899	. . 3 Trans $/\$
2		vex 2862	. . . . . . 7
3		vex 2862	. . . . . . 7
4	2, 3	opex 4588	. . . . . 6
5	4	elcompl 3225	. . . . 5 ∼ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c
6		elin 3219	. . . . . . . . . 10 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c Ins2 S $/\$ Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c
7	2	otelins2 5791	. . . . . . . . . . . 12 Ins2 S S
8		vex 2862	. . . . . . . . . . . . 13
9	8, 3	opelssetsn 4760	. . . . . . . . . . . 12 S
10	7, 9	bitri 240	. . . . . . . . . . 11 Ins2 S
11		elima1c 4947	. . . . . . . . . . . 12 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c
12		elin 3219	. . . . . . . . . . . . . 14 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c Ins2 Ins2 S $/\$ Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c
13		snex 4111	. . . . . . . . . . . . . . . . 17
14	13	otelins2 5791	. . . . . . . . . . . . . . . 16 Ins2 Ins2 S Ins2 S
15	2	otelins2 5791	. . . . . . . . . . . . . . . 16 Ins2 S S
16		vex 2862	. . . . . . . . . . . . . . . . 17
17	16, 3	opelssetsn 4760	. . . . . . . . . . . . . . . 16 S
18	14, 15, 17	3bitri 262	. . . . . . . . . . . . . . 15 Ins2 Ins2 S
19		elima1c 4947	. . . . . . . . . . . . . . . 16 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
20		elin 3219	. . . . . . . . . . . . . . . . . 18 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins2 Ins2 Ins2 S $/\$ Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
21		snex 4111	. . . . . . . . . . . . . . . . . . . . 21
22	21	otelins2 5791	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins2 Ins2 S Ins2 Ins2 S
23	13	otelins2 5791	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins2 S Ins2 S
24	2	otelins2 5791	. . . . . . . . . . . . . . . . . . . . 21 Ins2 S S
25		vex 2862	. . . . . . . . . . . . . . . . . . . . . 22
26	25, 3	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . 21 S
27	24, 26	bitri 240	. . . . . . . . . . . . . . . . . . . 20 Ins2 S
28	22, 23, 27	3bitri 262	. . . . . . . . . . . . . . . . . . 19 Ins2 Ins2 Ins2 S
29		eldif 3221	. . . . . . . . . . . . . . . . . . . 20 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c $/\$ Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
30		elin 3219	. . . . . . . . . . . . . . . . . . . . . 22 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
31		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . 25
32		opelxp 4811	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
33	31, 32	mpbiran 884	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
34	3	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S 1_c
35		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃ Ins2 Ins2 S Ins4 SI₃ $/\$ Ins2 Ins2 S
36	2	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins4 SI₃ SI₃
37	25, 16, 8	otsnelsi3 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI₃
38		oteltxp 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
39		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
40		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
41		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
42	40, 41	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
43	39, 42	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
44	8, 16	op1st2nd 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
45	38, 43, 44	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
46	36, 37, 45	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃
47	21	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 Ins2 S Ins2 S
48	13	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 S S
49	25, 2	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 S
50	47, 48, 49	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 S
51	46, 50	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃ $/\$ Ins2 Ins2 S $/\$
52	35, 51	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ Ins2 Ins2 S $/\$
53	52	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ Ins2 Ins2 S $/\$
54		elima1c 4947	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S
55		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
57	55, 56	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
58	53, 54, 57	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 S 1_c
59	33, 34, 58	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
60		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins3 S
61	13, 4	opex 4588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
62	61	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃ SI₃
63		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63, 25, 16	otsnelsi3 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃
65		oteltxp 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
67		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69	67, 68	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
70	66, 69	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
71	16, 25	op1st2nd 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
72	65, 70, 71	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	62, 64, 72	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃
74	31	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins3 S
75	21	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 Ins3 S Ins2 Ins3 S
76	13	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 Ins3 S Ins3 S
77	3	otelins3 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3 S S
78	63, 2	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 S
79	76, 77, 78	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins3 S
80	74, 75, 79	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2 Ins2 Ins2 Ins3 S
81	73, 80	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins3 S $/\$
82	60, 81	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S $/\$
83	82	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S $/\$
84		elima1c 4947	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S
85		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . 25
86		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
87	85, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
88	83, 84, 87	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
89	59, 88	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
90	30, 89	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
91	21	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
92	3	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S 1_c
93		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ Ins2 Ins2 S Ins4 SI₃ $/\$ Ins2 Ins2 S
94	2	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃ SI₃
95	16, 25, 8	otsnelsi3 5805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI₃
96		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
97		oteltxp 5782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
98		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
99		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
100	98, 99	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
101	96, 97, 100	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
102	8, 25	op1st2nd 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
103	95, 101, 102	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃
104	94, 103	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃
105	31	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 S Ins2 S
106	13	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 S S
107	16, 2	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 S
108	105, 106, 107	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2 Ins2 S
109	104, 108	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ $/\$ Ins2 Ins2 S $/\$
110	93, 109	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ Ins2 Ins2 S $/\$
111	110	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 S $/\$
112		elima1c 4947	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S
113		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . . . 25
114		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
115	113, 114	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
116	111, 112, 115	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 SI₃ Ins2 Ins2 S 1_c
117	91, 92, 116	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
118	117	notbii 287	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
119	90, 118	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c $/\$ Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ $/\$
120	29, 119	bitri 240	. . . . . . . . . . . . . . . . . . 19 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ $/\$
121	28, 120	anbi12i 678	. . . . . . . . . . . . . . . . . 18 Ins2 Ins2 Ins2 S $/\$ Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ $/\$ $/\$
122	20, 121	bitri 240	. . . . . . . . . . . . . . . . 17 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ $/\$ $/\$
123	122	exbii 1582	. . . . . . . . . . . . . . . 16 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c $/\$ $/\$ $/\$
124		df-rex 2620	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
125		rexanali 2660	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
126	124, 125	bitr3i 242	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
127	19, 123, 126	3bitri 262	. . . . . . . . . . . . . . 15 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c $/\$
128	18, 127	anbi12i 678	. . . . . . . . . . . . . 14 Ins2 Ins2 S $/\$ Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c $/\$ $/\$
129	12, 128	bitri 240	. . . . . . . . . . . . 13 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c $/\$ $/\$
130	129	exbii 1582	. . . . . . . . . . . 12 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c $/\$ $/\$
131		df-rex 2620	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		rexnal 2625	. . . . . . . . . . . . 13 $/\$ $/\$
133	131, 132	bitr3i 242	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
134	11, 130, 133	3bitri 262	. . . . . . . . . . 11 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c $/\$
135	10, 134	anbi12i 678	. . . . . . . . . 10 Ins2 S $/\$ Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c $/\$ $/\$
136	6, 135	bitri 240	. . . . . . . . 9 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c $/\$ $/\$
137	136	exbii 1582	. . . . . . . 8 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c $/\$ $/\$
138		elima1c 4947	. . . . . . . 8 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c
139		df-rex 2620	. . . . . . . 8 $/\$ $/\$ $/\$
140	137, 138, 139	3bitr4i 268	. . . . . . 7 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c $/\$
141		rexnal 2625	. . . . . . 7 $/\$ $/\$
142	140, 141	bitri 240	. . . . . 6 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c $/\$
143	142	con2bii 322	. . . . 5 $/\$ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c
144	5, 143	bitr4i 243	. . . 4 ∼ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c $/\$
145	144	opabbi2i 4866	. . 3 ∼ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c $/\$
146	1, 145	eqtr4i 2376	. 2 Trans ∼ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c
147		ssetex 4744	. . . . . 6 S
148	147	ins2ex 5797	. . . . 5 Ins2 S
149	148	ins2ex 5797	. . . . . . 7 Ins2 Ins2 S
150	149	ins2ex 5797	. . . . . . . . 9 Ins2 Ins2 Ins2 S
151		vvex 4109	. . . . . . . . . . . 12
152		2ndex 5112	. . . . . . . . . . . . . . . . . 18
153		1stex 4739	. . . . . . . . . . . . . . . . . 18
154	152, 153	txpex 5785	. . . . . . . . . . . . . . . . 17
155	154	si3ex 5806	. . . . . . . . . . . . . . . 16 SI₃
156	155	ins4ex 5799	. . . . . . . . . . . . . . 15 Ins4 SI₃
157	156, 149	inex 4105	. . . . . . . . . . . . . 14 Ins4 SI₃ Ins2 Ins2 S
158		1cex 4142	. . . . . . . . . . . . . 14 1_c
159	157, 158	imaex 4747	. . . . . . . . . . . . 13 Ins4 SI₃ Ins2 Ins2 S 1_c
160	159	ins4ex 5799	. . . . . . . . . . . 12 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
161	151, 160	xpex 5115	. . . . . . . . . . 11 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
162	147	ins3ex 5798	. . . . . . . . . . . . . . . 16 Ins3 S
163	162	ins2ex 5797	. . . . . . . . . . . . . . 15 Ins2 Ins3 S
164	163	ins2ex 5797	. . . . . . . . . . . . . 14 Ins2 Ins2 Ins3 S
165	164	ins2ex 5797	. . . . . . . . . . . . 13 Ins2 Ins2 Ins2 Ins3 S
166	156, 165	inex 4105	. . . . . . . . . . . 12 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S
167	166, 158	imaex 4747	. . . . . . . . . . 11 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
168	161, 167	inex 4105	. . . . . . . . . 10 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
169	160	ins2ex 5797	. . . . . . . . . 10 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
170	168, 169	difex 4107	. . . . . . . . 9 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
171	150, 170	inex 4105	. . . . . . . 8 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
172	171, 158	imaex 4747	. . . . . . 7 Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c
173	149, 172	inex 4105	. . . . . 6 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c
174	173, 158	imaex 4747	. . . . 5 Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c
175	148, 174	inex 4105	. . . 4 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c
176	175, 158	imaex 4747	. . 3 Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c
177	176	complex 4104	. 2 ∼ Ins2 S Ins2 Ins2 S Ins2 Ins2 Ins2 S Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c1_c1_c1_c
178	146, 177	eqeltri 2423	1 Trans

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

wral 2614

wrex 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cin 3208

csn 3737 1_cc1c 4134

cop 4561

copab 4622 class class class wbr 4639

c1st 4717 S csset 4719

cima 4722

cxp 4770

c2nd 4783

ctxp 5735 Ins2 cins2 5749 Ins3 cins3 5751 Ins4 cins4 5755 SI₃ csi3 5757 Trans ctrans 5888

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 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

W3C validator