transex - New Foundations Explorer

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

Theorem transex 5911

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 5900	. . 3 Trans $/\$
2		vex 2863	. . . . . . 7
3		vex 2863	. . . . . . 7
4	2, 3	opex 4589	. . . . . 6
5	4	elcompl 3226	. . . . 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 3220	. . . . . . . . . 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 5792	. . . . . . . . . . . 12 Ins2 S S
8		vex 2863	. . . . . . . . . . . . 13
9	8, 3	opelssetsn 4761	. . . . . . . . . . . 12 S
10	7, 9	bitri 240	. . . . . . . . . . 11 Ins2 S
11		elima1c 4948	. . . . . . . . . . . 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 3220	. . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . 17
14	13	otelins2 5792	. . . . . . . . . . . . . . . 16 Ins2 Ins2 S Ins2 S
15	2	otelins2 5792	. . . . . . . . . . . . . . . 16 Ins2 S S
16		vex 2863	. . . . . . . . . . . . . . . . 17
17	16, 3	opelssetsn 4761	. . . . . . . . . . . . . . . 16 S
18	14, 15, 17	3bitri 262	. . . . . . . . . . . . . . 15 Ins2 Ins2 S
19		elima1c 4948	. . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . 21
22	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins2 Ins2 S Ins2 Ins2 S
23	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins2 S Ins2 S
24	2	otelins2 5792	. . . . . . . . . . . . . . . . . . . . 21 Ins2 S S
25		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22
26	25, 3	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . 21 S
27	24, 26	bitri 240	. . . . . . . . . . . . . . . . . . . 20 Ins2 S
28	22, 23, 27	3bitri 262	. . . . . . . . . . . . . . . . . . 19 Ins2 Ins2 Ins2 S
29		eldif 3222	. . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25
32		opelxp 4812	. . . . . . . . . . . . . . . . . . . . . . . . 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 5795	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S 1_c
35		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃ Ins2 Ins2 S Ins4 SI₃ $/\$ Ins2 Ins2 S
36	2	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins4 SI₃ SI₃
37	25, 16, 8	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI₃
38		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
39		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
40		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
41		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
42	40, 41	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
43	39, 42	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
44	8, 16	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
45	38, 43, 44	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
46	36, 37, 45	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃
47	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 Ins2 S Ins2 S
48	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 S S
49	25, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4948	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S
55		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins3 S
61	13, 4	opex 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
62	61	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃ SI₃
63		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63, 25, 16	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃
65		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
67		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69	67, 68	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
70	66, 69	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
71	16, 25	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
72	65, 70, 71	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	62, 64, 72	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃
74	31	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins3 S
75	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 Ins3 S Ins2 Ins3 S
76	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2 Ins3 S Ins3 S
77	3	otelins3 5793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3 S S
78	63, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4948	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S
85		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . 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 5792	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
92	3	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S 1_c
93		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ Ins2 Ins2 S Ins4 SI₃ $/\$ Ins2 Ins2 S
94	2	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins4 SI₃ SI₃
95	16, 25, 8	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI₃
96		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
97		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
98		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
99		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
100	98, 99	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
101	96, 97, 100	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
102	8, 25	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
103	95, 101, 102	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃
104	94, 103	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃
105	31	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 Ins2 S Ins2 S
106	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2 S S
107	16, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4948	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 S
113		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
125		rexanali 2661	. . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		rexnal 2626	. . . . . . . . . . . . 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 4948	. . . . . . . 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 2621	. . . . . . . 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 2626	. . . . . . 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 4867	. . 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 4745	. . . . . 6 S
148	147	ins2ex 5798	. . . . 5 Ins2 S
149	148	ins2ex 5798	. . . . . . 7 Ins2 Ins2 S
150	149	ins2ex 5798	. . . . . . . . 9 Ins2 Ins2 Ins2 S
151		vvex 4110	. . . . . . . . . . . 12
152		2ndex 5113	. . . . . . . . . . . . . . . . . 18
153		1stex 4740	. . . . . . . . . . . . . . . . . 18
154	152, 153	txpex 5786	. . . . . . . . . . . . . . . . 17
155	154	si3ex 5807	. . . . . . . . . . . . . . . 16 SI₃
156	155	ins4ex 5800	. . . . . . . . . . . . . . 15 Ins4 SI₃
157	156, 149	inex 4106	. . . . . . . . . . . . . 14 Ins4 SI₃ Ins2 Ins2 S
158		1cex 4143	. . . . . . . . . . . . . 14 1_c
159	157, 158	imaex 4748	. . . . . . . . . . . . 13 Ins4 SI₃ Ins2 Ins2 S 1_c
160	159	ins4ex 5800	. . . . . . . . . . . 12 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
161	151, 160	xpex 5116	. . . . . . . . . . 11 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
162	147	ins3ex 5799	. . . . . . . . . . . . . . . 16 Ins3 S
163	162	ins2ex 5798	. . . . . . . . . . . . . . 15 Ins2 Ins3 S
164	163	ins2ex 5798	. . . . . . . . . . . . . 14 Ins2 Ins2 Ins3 S
165	164	ins2ex 5798	. . . . . . . . . . . . 13 Ins2 Ins2 Ins2 Ins3 S
166	156, 165	inex 4106	. . . . . . . . . . . 12 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S
167	166, 158	imaex 4748	. . . . . . . . . . 11 Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
168	161, 167	inex 4106	. . . . . . . . . 10 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins3 S 1_c
169	160	ins2ex 5798	. . . . . . . . . 10 Ins2 Ins4 Ins4 SI₃ Ins2 Ins2 S 1_c
170	168, 169	difex 4108	. . . . . . . . 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 4106	. . . . . . . 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 4748	. . . . . . 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 4106	. . . . . 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 4748	. . . . 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 4106	. . . 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 4748	. . 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 4105	. 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

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

wral 2615

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cin 3209

csn 3738 1_cc1c 4135

cop 4562

copab 4623 class class class wbr 4640

c1st 4718 S csset 4720

cima 4723

cxp 4771

c2nd 4784

ctxp 5736 Ins2 cins2 5750 Ins3 cins3 5752 Ins4 cins4 5756 SI₃ csi3 5758 Trans ctrans 5889

This proof depends on 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 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This proof 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 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-xp 4785 df-cnv 4786 df-2nd 4798 df-txp 5737 df-ins2 5751 df-ins3 5753 df-ins4 5757 df-si3 5759 df-trans 5900

This theorem is used by: partialex 5918 erex 5921

W3C validator