Theorem truni 3425

Description: The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.)

Assertion

Ref	Expression
truni	|- (A.x e. A Tr x -> Tr U.A)

Distinct variable group:   x,A

Proof of Theorem truni

Step	Hyp	Ref	Expression
1		dftr3 3415	. . . . . . . . 9 |- (Tr x <-> A.y e. x y C_ x)
2	1	biimpi 168	. . . . . . . 8 |- (Tr x -> A.y e. x y C_ x)
3	2	a1i 8	. . . . . . 7 |- (x e. A -> (Tr x -> A.y e. x y C_ x))
4		ax-17 1317	. . . . . . . 8 |- (x e. A -> A.y x e. A)
5		alral 2153	. . . . . . . 8 |- (A.y x e. A -> A.y e. x x e. A)
6	4, 5	syl 12	. . . . . . 7 |- (x e. A -> A.y e. x x e. A)
7	3, 6	jctird 663	. . . . . 6 |- (x e. A -> (Tr x -> (A.y e. x y C_ x /\ A.y e. x x e. A)))
8		r19.26 2219	. . . . . 6 |- (A.y e. x (y C_ x /\ x e. A) <-> (A.y e. x y C_ x /\ A.y e. x x e. A))
9	7, 8	syl6ibr 230	. . . . 5 |- (x e. A -> (Tr x -> A.y e. x (y C_ x /\ x e. A)))
10		ssuni 3201	. . . . . 6 |- ((y C_ x /\ x e. A) -> y C_ U.A)
11	10	ralimi 2168	. . . . 5 |- (A.y e. x (y C_ x /\ x e. A) -> A.y e. x y C_ U.A)
12	9, 11	syl6 25	. . . 4 |- (x e. A -> (Tr x -> A.y e. x y C_ U.A))
13	12	ralimia 2166	. . 3 |- (A.x e. A Tr x -> A.x e. A A.y e. x y C_ U.A)
14		df-ral 2109	. . . . 5 |- (A.y e. x y C_ U.A <-> A.y(y e. x -> y C_ U.A))
15	14	ralbii 2127	. . . 4 |- (A.x e. A A.y e. x y C_ U.A <-> A.x e. A A.y(y e. x -> y C_ U.A))
16		ralcom4 2310	. . . 4 |- (A.x e. A A.y(y e. x -> y C_ U.A) <-> A.yA.x e. A (y e. x -> y C_ U.A))
17	15, 16	bitr2i 191	. . 3 |- (A.yA.x e. A (y e. x -> y C_ U.A) <-> A.x e. A A.y e. x y C_ U.A)
18	13, 17	sylibr 217	. 2 |- (A.x e. A Tr x -> A.yA.x e. A (y e. x -> y C_ U.A))
19		dftr3 3415	. . 3 |- (Tr U.A <-> A.y e. U.Ay C_ U.A)
20		df-ral 2109	. . 3 |- (A.y e. U.Ay C_ U.A <-> A.y(y e. U.A -> y C_ U.A))
21		eluni2 3181	. . . . . 6 |- (y e. U.A <-> E.x e. A y e. x)
22	21	imbi1i 203	. . . . 5 |- ((y e. U.A -> y C_ U.A) <-> (E.x e. A y e. x -> y C_ U.A))
23		r19.23v 2208	. . . . 5 |- (A.x e. A (y e. x -> y C_ U.A) <-> (E.x e. A y e. x -> y C_ U.A))
24	22, 23	bitr4i 193	. . . 4 |- ((y e. U.A -> y C_ U.A) <-> A.x e. A (y e. x -> y C_ U.A))
25	24	albii 1346	. . 3 |- (A.y(y e. U.A -> y C_ U.A) <-> A.yA.x e. A (y e. x -> y C_ U.A))
26	19, 20, 25	3bitri 194	. 2 |- (Tr U.A <-> A.yA.x e. A (y e. x -> y C_ U.A))
27	18, 26	sylibr 217	1 |- (A.x e. A Tr x -> Tr U.A)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  U.cuni 3177  Tr wtr 3411

This theorem is referenced by:  dfon2lem1 13849

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178  df-tr 3412

Copyright terms: Public domain