Theorem transex 5911

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.

Step	Hyp	Ref	Expression
1		df-trans 5900	. . 3 ⊢ Trans = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)}
2		vex 2863	. . . . . . 7 ⊢ r ∈ V
3		vex 2863	. . . . . . 7 ⊢ a ∈ V
4	2, 3	opex 4589	. . . . . 6 ⊢ ⟨r, a⟩ ∈ V
5	4	elcompl 3226	. . . . 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 3220	. . . . . . . . . 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)))
7	2	otelins2 5792	. . . . . . . . . . . 12 ⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ ⟨{x}, a⟩ ∈ S )
8		vex 2863	. . . . . . . . . . . . 13 ⊢ x ∈ V
9	8, 3	opelssetsn 4761	. . . . . . . . . . . 12 ⊢ (⟨{x}, a⟩ ∈ S ↔ x ∈ a)
10	7, 9	bitri 240	. . . . . . . . . . 11 ⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ x ∈ a)
11		elima1c 4948	. . . . . . . . . . . 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 3220	. . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . 17 ⊢ {x} ∈ V
14	13	otelins2 5792	. . . . . . . . . . . . . . . 16 ⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{y}, ⟨r, a⟩⟩ ∈ Ins2 S )
15	2	otelins2 5792	. . . . . . . . . . . . . . . 16 ⊢ (⟨{y}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ ⟨{y}, a⟩ ∈ S )
16		vex 2863	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
17	16, 3	opelssetsn 4761	. . . . . . . . . . . . . . . 16 ⊢ (⟨{y}, a⟩ ∈ S ↔ y ∈ a)
18	14, 15, 17	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ↔ y ∈ a)
19		elima1c 4948	. . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {y} ∈ V
22	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins2 S ↔ ⟨{z}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S )
23	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨{z}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{z}, ⟨r, a⟩⟩ ∈ Ins2 S )
24	2	otelins2 5792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨{z}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ ⟨{z}, a⟩ ∈ S )
25		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ z ∈ V
26	25, 3	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨{z}, a⟩ ∈ S ↔ z ∈ a)
27	24, 26	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨{z}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ z ∈ a)
28	22, 23, 27	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins2 S ↔ z ∈ a)
29		eldif 3222	. . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {z} ∈ V
32		opelxp 4812	. . . . . . . . . . . . . . . . . . . . . . . . 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)))
33	31, 32	mpbiran 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))
34	3	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ))
36	2	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ ⟨{z}, ⟨{y}, {x}⟩⟩ ∈ SI3 (2nd ⊗ 1st ))
37	25, 16, 8	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{z}, ⟨{y}, {x}⟩⟩ ∈ SI3 (2nd ⊗ 1st ) ↔ ⟨z, ⟨y, x⟩⟩ ∈ (2nd ⊗ 1st ))
38		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (z1st x ↔ ⟨z, x⟩ ∈ 1st )
41		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (z2nd y ↔ ⟨z, y⟩ ∈ 2nd )
42	40, 41	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((z1st x ∧ z2nd y) ↔ (⟨z, x⟩ ∈ 1st ∧ ⟨z, y⟩ ∈ 2nd ))
43	39, 42	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⟨z, y⟩ ∈ 2nd ∧ ⟨z, x⟩ ∈ 1st ) ↔ (z1st x ∧ z2nd y))
44	8, 16	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((z1st x ∧ z2nd y) ↔ z = ⟨x, y⟩)
45	38, 43, 44	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨z, ⟨y, x⟩⟩ ∈ (2nd ⊗ 1st ) ↔ z = ⟨x, y⟩)
46	36, 37, 45	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ z = ⟨x, y⟩)
47	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{z}, ⟨{x}, r⟩⟩ ∈ Ins2 S )
48	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{z}, ⟨{x}, r⟩⟩ ∈ Ins2 S ↔ ⟨{z}, r⟩ ∈ S )
49	25, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{z}, r⟩ ∈ S ↔ z ∈ r)
50	47, 48, 49	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ z ∈ r)
51	46, 50	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ∧ ⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ) ↔ (z = ⟨x, y⟩ ∧ z ∈ r))
52	35, 51	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ (z = ⟨x, y⟩ ∧ z ∈ r))
53	52	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃z⟨{z}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ ∃z(z = ⟨x, y⟩ ∧ z ∈ r))
54		elima1c 4948	. . . . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (xry ↔ ⟨x, y⟩ ∈ r)
56		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨x, y⟩ ∈ r ↔ ∃z(z = ⟨x, y⟩ ∧ z ∈ r))
57	55, 56	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (xry ↔ ∃z(z = ⟨x, y⟩ ∧ z ∈ r))
58	53, 54, 57	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xry)
59	33, 34, 58	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ xry)
60		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ))
61	13, 4	opex 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨{x}, ⟨r, a⟩⟩ ∈ V
62	61	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{q}, ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ ⟨{q}, ⟨{z}, {y}⟩⟩ ∈ SI3 (2nd ⊗ 1st ))
63		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ q ∈ V
64	63, 25, 16	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{q}, ⟨{z}, {y}⟩⟩ ∈ SI3 (2nd ⊗ 1st ) ↔ ⟨q, ⟨z, y⟩⟩ ∈ (2nd ⊗ 1st ))
65		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (q1st y ↔ ⟨q, y⟩ ∈ 1st )
68		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (q2nd z ↔ ⟨q, z⟩ ∈ 2nd )
69	67, 68	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((q1st y ∧ q2nd z) ↔ (⟨q, y⟩ ∈ 1st ∧ ⟨q, z⟩ ∈ 2nd ))
70	66, 69	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨q, z⟩ ∈ 2nd ∧ ⟨q, y⟩ ∈ 1st ) ↔ (q1st y ∧ q2nd z))
71	16, 25	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((q1st y ∧ q2nd z) ↔ q = ⟨y, z⟩)
72	65, 70, 71	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨q, ⟨z, y⟩⟩ ∈ (2nd ⊗ 1st ) ↔ q = ⟨y, z⟩)
73	62, 64, 72	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨{q}, ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ q = ⟨y, z⟩)
74	31	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{q}, ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins2 Ins3 S ↔ ⟨{q}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins3 S )
75	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{q}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins3 S ↔ ⟨{q}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins3 S )
76	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{q}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins3 S ↔ ⟨{q}, ⟨r, a⟩⟩ ∈ Ins3 S )
77	3	otelins3 5793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{q}, ⟨r, a⟩⟩ ∈ Ins3 S ↔ ⟨{q}, r⟩ ∈ S )
78	63, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨{q}, r⟩ ∈ S ↔ q ∈ r)
79	76, 77, 78	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{q}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins3 S ↔ q ∈ r)
80	74, 75, 79	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨{q}, ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩⟩ ∈ Ins2 Ins2 Ins2 Ins3 S ↔ q ∈ r)
81	73, 80	anbi12i 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))
82	60, 81	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨{q}, ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩⟩ ∈ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ (q = ⟨y, z⟩ ∧ q ∈ r))
83	82	exbii 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 4948	. . . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (yrz ↔ ⟨y, z⟩ ∈ r)
86		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨y, z⟩ ∈ r ↔ ∃q(q = ⟨y, z⟩ ∧ q ∈ r))
87	85, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (yrz ↔ ∃q(q = ⟨y, z⟩ ∧ q ∈ r))
88	83, 84, 87	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ↔ yrz)
89	59, 88	anbi12i 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))
90	30, 89	bitri 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))
91	21	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . 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))
92	3	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ))
94	2	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ ⟨{y}, ⟨{z}, {x}⟩⟩ ∈ SI3 (2nd ⊗ 1st ))
95	16, 25, 8	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨y, ⟨z, x⟩⟩ ∈ (2nd ⊗ 1st ) ↔ (⟨y, z⟩ ∈ 2nd ∧ ⟨y, x⟩ ∈ 1st ))
98		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (y1st x ↔ ⟨y, x⟩ ∈ 1st )
99		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (y2nd z ↔ ⟨y, z⟩ ∈ 2nd )
100	98, 99	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((y1st x ∧ y2nd z) ↔ (⟨y, x⟩ ∈ 1st ∧ ⟨y, z⟩ ∈ 2nd ))
101	96, 97, 100	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨y, ⟨z, x⟩⟩ ∈ (2nd ⊗ 1st ) ↔ (y1st x ∧ y2nd z))
102	8, 25	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((y1st x ∧ y2nd z) ↔ y = ⟨x, z⟩)
103	95, 101, 102	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{y}, ⟨{z}, {x}⟩⟩ ∈ SI3 (2nd ⊗ 1st ) ↔ y = ⟨x, z⟩)
104	94, 103	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ↔ y = ⟨x, z⟩)
105	31	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{y}, ⟨{x}, r⟩⟩ ∈ Ins2 S )
106	13	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ Ins2 S ↔ ⟨{y}, r⟩ ∈ S )
107	16, 2	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨{y}, r⟩ ∈ S ↔ y ∈ r)
108	105, 106, 107	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ y ∈ r)
109	104, 108	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 (2nd ⊗ 1st ) ∧ ⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ) ↔ (y = ⟨x, z⟩ ∧ y ∈ r))
110	93, 109	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ (y = ⟨x, z⟩ ∧ y ∈ r))
111	110	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃y⟨{y}, ⟨{z}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ↔ ∃y(y = ⟨x, z⟩ ∧ y ∈ r))
112		elima1c 4948	. . . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (xrz ↔ ⟨x, z⟩ ∈ r)
114		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨x, z⟩ ∈ r ↔ ∃y(y = ⟨x, z⟩ ∧ y ∈ r))
115	113, 114	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (xrz ↔ ∃y(y = ⟨x, z⟩ ∧ y ∈ r))
116	111, 112, 115	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨{z}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz)
117	91, 92, 116	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz)
118	117	notbii 287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ⟨{z}, ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩⟩ ∈ Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ ¬ xrz)
119	90, 118	anbi12i 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))
120	29, 119	bitri 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))
121	28, 120	anbi12i 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)))
122	20, 121	bitri 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)))
123	122	exbii 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 2621	. . . . . . . . . . . . . . . . 17 ⊢ (∃z ∈ a ((xry ∧ yrz) ∧ ¬ xrz) ↔ ∃z(z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz)))
125		rexanali 2661	. . . . . . . . . . . . . . . . 17 ⊢ (∃z ∈ a ((xry ∧ yrz) ∧ ¬ xrz) ↔ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))
126	124, 125	bitr3i 242	. . . . . . . . . . . . . . . 16 ⊢ (∃z(z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz)) ↔ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))
127	19, 123, 126	3bitri 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))
128	18, 127	anbi12i 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)))
129	12, 128	bitri 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)))
130	129	exbii 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 2621	. . . . . . . . . . . . 13 ⊢ (∃y ∈ a ¬ ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ∃y(y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)))
132		rexnal 2626	. . . . . . . . . . . . 13 ⊢ (∃y ∈ a ¬ ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))
133	131, 132	bitr3i 242	. . . . . . . . . . . 12 ⊢ (∃y(y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)) ↔ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))
134	11, 130, 133	3bitri 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))
135	10, 134	anbi12i 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)))
136	6, 135	bitri 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)))
137	136	exbii 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 4948	. . . . . . . 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 2621	. . . . . . . 8 ⊢ (∃x ∈ a ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)))
140	137, 138, 139	3bitr4i 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 2626	. . . . . . 7 ⊢ (∃x ∈ a ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ¬ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))
142	140, 141	bitri 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))
143	142	con2bii 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))
144	5, 143	bitr4i 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))
145	144	opabbi2i 4867	. . 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)}
146	1, 145	eqtr4i 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 4745	. . . . . 6 ⊢ S ∈ V
148	147	ins2ex 5798	. . . . 5 ⊢ Ins2 S ∈ V
149	148	ins2ex 5798	. . . . . . 7 ⊢ Ins2 Ins2 S ∈ V
150	149	ins2ex 5798	. . . . . . . . 9 ⊢ Ins2 Ins2 Ins2 S ∈ V
151		vvex 4110	. . . . . . . . . . . 12 ⊢ V ∈ V
152		2ndex 5113	. . . . . . . . . . . . . . . . . 18 ⊢ 2nd ∈ V
153		1stex 4740	. . . . . . . . . . . . . . . . . 18 ⊢ 1st ∈ V
154	152, 153	txpex 5786	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ⊗ 1st ) ∈ V
155	154	si3ex 5807	. . . . . . . . . . . . . . . 16 ⊢ SI3 (2nd ⊗ 1st ) ∈ V
156	155	ins4ex 5800	. . . . . . . . . . . . . . 15 ⊢ Ins4 SI3 (2nd ⊗ 1st ) ∈ V
157	156, 149	inex 4106	. . . . . . . . . . . . . 14 ⊢ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ∈ V
158		1cex 4143	. . . . . . . . . . . . . 14 ⊢ 1c ∈ V
159	157, 158	imaex 4748	. . . . . . . . . . . . 13 ⊢ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ∈ V
160	159	ins4ex 5800	. . . . . . . . . . . 12 ⊢ Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ∈ V
161	151, 160	xpex 5116	. . . . . . . . . . 11 ⊢ (V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∈ V
162	147	ins3ex 5799	. . . . . . . . . . . . . . . 16 ⊢ Ins3 S ∈ V
163	162	ins2ex 5798	. . . . . . . . . . . . . . 15 ⊢ Ins2 Ins3 S ∈ V
164	163	ins2ex 5798	. . . . . . . . . . . . . 14 ⊢ Ins2 Ins2 Ins3 S ∈ V
165	164	ins2ex 5798	. . . . . . . . . . . . 13 ⊢ Ins2 Ins2 Ins2 Ins3 S ∈ V
166	156, 165	inex 4106	. . . . . . . . . . . 12 ⊢ ( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ∈ V
167	166, 158	imaex 4748	. . . . . . . . . . 11 ⊢ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ∈ V
168	161, 167	inex 4106	. . . . . . . . . 10 ⊢ ((V × Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∩ (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ∈ V
169	160	ins2ex 5798	. . . . . . . . . 10 ⊢ Ins2 Ins4 (( Ins4 SI3 (2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ∈ V
170	168, 169	difex 4108	. . . . . . . . 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
171	150, 170	inex 4106	. . . . . . . 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
172	171, 158	imaex 4748	. . . . . . 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
173	149, 172	inex 4106	. . . . . 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
174	173, 158	imaex 4748	. . . . 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
175	148, 174	inex 4106	. . . 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
176	175, 158	imaex 4748	. . 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
177	176	complex 4105	. 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
178	146, 177	eqeltri 2423	1 ⊢ Trans ∈ V

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∀wral 2615  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∩ cin 3209  {csn 3738  1_cc1c 4135  ⟨cop 4562  {copab 4623   class class class wbr 4640  1^st c1st 4718   S csset 4720   “ cima 4723   × cxp 4771  2^nd 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