r1tr

Description: The cumulative hierarchy of sets is transitive. Lemma 7T of Enderton p. 202. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1tr	$⊢ Tr R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpri	$⊢ Lim dom R_{1}$
3		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
4		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
5	2 3 4	mp2b	$⊢ dom R_{1} \subseteq On$
6	5	sseli	$⊢ A \in dom R_{1} \to A \in On$
7		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
8		r10	$⊢ R_{1} (\emptyset) = \emptyset$
9	7 8	eqtrdi	$⊢ x = \emptyset \to R_{1} (x) = \emptyset$
10		treq	$⊢ R_{1} (x) = \emptyset \to (Tr R_{1} (x) \leftrightarrow Tr \emptyset)$
11	9 10	syl	$⊢ x = \emptyset \to (Tr R_{1} (x) \leftrightarrow Tr \emptyset)$
12		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
13		treq	$⊢ R_{1} (x) = R_{1} (y) \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (y))$
14	12 13	syl	$⊢ x = y \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (y))$
15		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
16		treq	$⊢ R_{1} (x) = R_{1} (suc y) \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (suc y))$
17	15 16	syl	$⊢ x = suc y \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (suc y))$
18		fveq2	$⊢ x = A \to R_{1} (x) = R_{1} (A)$
19		treq	$⊢ R_{1} (x) = R_{1} (A) \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (A))$
20	18 19	syl	$⊢ x = A \to (Tr R_{1} (x) \leftrightarrow Tr R_{1} (A))$
21		tr0	$⊢ Tr \emptyset$
22		limsuc	$⊢ Lim dom R_{1} \to (y \in dom R_{1} \leftrightarrow suc y \in dom R_{1})$
23	2 22	ax-mp	$⊢ y \in dom R_{1} \leftrightarrow suc y \in dom R_{1}$
24		simpr	$⊢ (y \in On \land Tr R_{1} (y)) \to Tr R_{1} (y)$
25		pwtr	$⊢ Tr R_{1} (y) \leftrightarrow Tr 𝒫 R_{1} (y)$
26	24 25	sylib	$⊢ (y \in On \land Tr R_{1} (y)) \to Tr 𝒫 R_{1} (y)$
27		r1sucg	$⊢ y \in dom R_{1} \to R_{1} (suc y) = 𝒫 R_{1} (y)$
28		treq	$⊢ R_{1} (suc y) = 𝒫 R_{1} (y) \to (Tr R_{1} (suc y) \leftrightarrow Tr 𝒫 R_{1} (y))$
29	27 28	syl	$⊢ y \in dom R_{1} \to (Tr R_{1} (suc y) \leftrightarrow Tr 𝒫 R_{1} (y))$
30	26 29	syl5ibrcom	$⊢ (y \in On \land Tr R_{1} (y)) \to (y \in dom R_{1} \to Tr R_{1} (suc y))$
31	23 30	syl5bir	$⊢ (y \in On \land Tr R_{1} (y)) \to (suc y \in dom R_{1} \to Tr R_{1} (suc y))$
32		ndmfv	$⊢ \neg suc y \in dom R_{1} \to R_{1} (suc y) = \emptyset$
33		treq	$⊢ R_{1} (suc y) = \emptyset \to (Tr R_{1} (suc y) \leftrightarrow Tr \emptyset)$
34	32 33	syl	$⊢ \neg suc y \in dom R_{1} \to (Tr R_{1} (suc y) \leftrightarrow Tr \emptyset)$
35	21 34	mpbiri	$⊢ \neg suc y \in dom R_{1} \to Tr R_{1} (suc y)$
36	31 35	pm2.61d1	$⊢ (y \in On \land Tr R_{1} (y)) \to Tr R_{1} (suc y)$
37	36	ex	$⊢ y \in On \to (Tr R_{1} (y) \to Tr R_{1} (suc y))$
38		triun	$⊢ \forall y \in x Tr R_{1} (y) \to Tr ⋃_{y \in x} R_{1} (y)$
39		r1limg	$⊢ (x \in dom R_{1} \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
40	39	ancoms	$⊢ (Lim x \land x \in dom R_{1}) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
41		treq	$⊢ R_{1} (x) = ⋃_{y \in x} R_{1} (y) \to (Tr R_{1} (x) \leftrightarrow Tr ⋃_{y \in x} R_{1} (y))$
42	40 41	syl	$⊢ (Lim x \land x \in dom R_{1}) \to (Tr R_{1} (x) \leftrightarrow Tr ⋃_{y \in x} R_{1} (y))$
43	38 42	syl5ibr	$⊢ (Lim x \land x \in dom R_{1}) \to (\forall y \in x Tr R_{1} (y) \to Tr R_{1} (x))$
44	43	impancom	$⊢ (Lim x \land \forall y \in x Tr R_{1} (y)) \to (x \in dom R_{1} \to Tr R_{1} (x))$
45		ndmfv	$⊢ \neg x \in dom R_{1} \to R_{1} (x) = \emptyset$
46	45 10	syl	$⊢ \neg x \in dom R_{1} \to (Tr R_{1} (x) \leftrightarrow Tr \emptyset)$
47	21 46	mpbiri	$⊢ \neg x \in dom R_{1} \to Tr R_{1} (x)$
48	44 47	pm2.61d1	$⊢ (Lim x \land \forall y \in x Tr R_{1} (y)) \to Tr R_{1} (x)$
49	48	ex	$⊢ Lim x \to (\forall y \in x Tr R_{1} (y) \to Tr R_{1} (x))$
50	11 14 17 20 21 37 49	tfinds	$⊢ A \in On \to Tr R_{1} (A)$
51	6 50	syl	$⊢ A \in dom R_{1} \to Tr R_{1} (A)$
52		ndmfv	$⊢ \neg A \in dom R_{1} \to R_{1} (A) = \emptyset$
53		treq	$⊢ R_{1} (A) = \emptyset \to (Tr R_{1} (A) \leftrightarrow Tr \emptyset)$
54	52 53	syl	$⊢ \neg A \in dom R_{1} \to (Tr R_{1} (A) \leftrightarrow Tr \emptyset)$
55	21 54	mpbiri	$⊢ \neg A \in dom R_{1} \to Tr R_{1} (A)$
56	51 55	pm2.61i	$⊢ Tr R_{1} (A)$

Metamath Proof Explorer

Theorem r1tr

Proof