r1tr

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

Metamath Proof Explorer

Theorem r1tr

Proof