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		pwtr	$⊢ Tr R_{1} (y) \leftrightarrow Tr 𝒫 R_{1} (y)$
25	24	bilani	$⊢ (y \in On \land Tr R_{1} (y)) \to Tr 𝒫 R_{1} (y)$
26		r1sucg	$⊢ y \in dom R_{1} \to R_{1} (suc y) = 𝒫 R_{1} (y)$
27		treq	$⊢ R_{1} (suc y) = 𝒫 R_{1} (y) \to (Tr R_{1} (suc y) \leftrightarrow Tr 𝒫 R_{1} (y))$
28	26 27	syl	$⊢ y \in dom R_{1} \to (Tr R_{1} (suc y) \leftrightarrow Tr 𝒫 R_{1} (y))$
29	25 28	syl5ibrcom	$⊢ (y \in On \land Tr R_{1} (y)) \to (y \in dom R_{1} \to Tr R_{1} (suc y))$
30	23 29	biimtrrid	$⊢ (y \in On \land Tr R_{1} (y)) \to (suc y \in dom R_{1} \to Tr R_{1} (suc y))$
31		ndmfv	$⊢ \neg suc y \in dom R_{1} \to R_{1} (suc y) = \emptyset$
32		treq	$⊢ R_{1} (suc y) = \emptyset \to (Tr R_{1} (suc y) \leftrightarrow Tr \emptyset)$
33	31 32	syl	$⊢ \neg suc y \in dom R_{1} \to (Tr R_{1} (suc y) \leftrightarrow Tr \emptyset)$
34	21 33	mpbiri	$⊢ \neg suc y \in dom R_{1} \to Tr R_{1} (suc y)$
35	30 34	pm2.61d1	$⊢ (y \in On \land Tr R_{1} (y)) \to Tr R_{1} (suc y)$
36	35	ex	$⊢ y \in On \to (Tr R_{1} (y) \to Tr R_{1} (suc y))$
37		triun	$⊢ \forall y \in x Tr R_{1} (y) \to Tr ⋃_{y \in x} R_{1} (y)$
38		r1limg	$⊢ (x \in dom R_{1} \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
39	38	ancoms	$⊢ (Lim x \land x \in dom R_{1}) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
40		treq	$⊢ R_{1} (x) = ⋃_{y \in x} R_{1} (y) \to (Tr R_{1} (x) \leftrightarrow Tr ⋃_{y \in x} R_{1} (y))$
41	39 40	syl	$⊢ (Lim x \land x \in dom R_{1}) \to (Tr R_{1} (x) \leftrightarrow Tr ⋃_{y \in x} R_{1} (y))$
42	37 41	imbitrrid	$⊢ (Lim x \land x \in dom R_{1}) \to (\forall y \in x Tr R_{1} (y) \to Tr R_{1} (x))$
43	42	impancom	$⊢ (Lim x \land \forall y \in x Tr R_{1} (y)) \to (x \in dom R_{1} \to Tr R_{1} (x))$
44		ndmfv	$⊢ \neg x \in dom R_{1} \to R_{1} (x) = \emptyset$
45	44 10	syl	$⊢ \neg x \in dom R_{1} \to (Tr R_{1} (x) \leftrightarrow Tr \emptyset)$
46	21 45	mpbiri	$⊢ \neg x \in dom R_{1} \to Tr R_{1} (x)$
47	43 46	pm2.61d1	$⊢ (Lim x \land \forall y \in x Tr R_{1} (y)) \to Tr R_{1} (x)$
48	47	ex	$⊢ Lim x \to (\forall y \in x Tr R_{1} (y) \to Tr R_{1} (x))$
49	11 14 17 20 21 36 48	tfinds	$⊢ A \in On \to Tr R_{1} (A)$
50	6 49	syl	$⊢ A \in dom R_{1} \to Tr R_{1} (A)$
51		ndmfv	$⊢ \neg A \in dom R_{1} \to R_{1} (A) = \emptyset$
52		treq	$⊢ R_{1} (A) = \emptyset \to (Tr R_{1} (A) \leftrightarrow Tr \emptyset)$
53	51 52	syl	$⊢ \neg A \in dom R_{1} \to (Tr R_{1} (A) \leftrightarrow Tr \emptyset)$
54	21 53	mpbiri	$⊢ \neg A \in dom R_{1} \to Tr R_{1} (A)$
55	50 54	pm2.61i	$⊢ Tr R_{1} (A)$

Metamath Proof Explorer

Theorem r1tr

Proof