Theorem 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 ( 𝑅1 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2	1	simpri	⊢ Lim dom 𝑅1
3		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4		ordsson	⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
5	2 3 4	mp2b	⊢ dom 𝑅1 ⊆ On
6	5	sseli	⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On )
7		fveq2	⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
8		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
9	7 8	eqtrdi	⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ∅ )
10		treq	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ∅ → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∅ ) )
11	9 10	syl	⊢ ( 𝑥 = ∅ → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∅ ) )
12		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
13		treq	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ 𝑦 ) ) )
14	12 13	syl	⊢ ( 𝑥 = 𝑦 → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ 𝑦 ) ) )
15		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
16		treq	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
17	15 16	syl	⊢ ( 𝑥 = suc 𝑦 → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
18		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝐴 ) )
19		treq	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝐴 ) → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ 𝐴 ) ) )
20	18 19	syl	⊢ ( 𝑥 = 𝐴 → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ( 𝑅1 ‘ 𝐴 ) ) )
21		tr0	⊢ Tr ∅
22		limsuc	⊢ ( Lim dom 𝑅1 → ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 ) )
23	2 22	ax-mp	⊢ ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 )
24		pwtr	⊢ ( Tr ( 𝑅1 ‘ 𝑦 ) ↔ Tr 𝒫 ( 𝑅1 ‘ 𝑦 ) )
25	24	bilani	⊢ ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1 ‘ 𝑦 ) ) → Tr 𝒫 ( 𝑅1 ‘ 𝑦 ) )
26		r1sucg	⊢ ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
27		treq	⊢ ( ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr 𝒫 ( 𝑅1 ‘ 𝑦 ) ) )
28	26 27	syl	⊢ ( 𝑦 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr 𝒫 ( 𝑅1 ‘ 𝑦 ) ) )
29	25 28	syl5ibrcom	⊢ ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
30	23 29	biimtrrid	⊢ ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
31		ndmfv	⊢ ( ¬ suc 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑦 ) = ∅ )
32		treq	⊢ ( ( 𝑅1 ‘ suc 𝑦 ) = ∅ → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr ∅ ) )
33	31 32	syl	⊢ ( ¬ suc 𝑦 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr ∅ ) )
34	21 33	mpbiri	⊢ ( ¬ suc 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) )
35	30 34	pm2.61d1	⊢ ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1 ‘ 𝑦 ) ) → Tr ( 𝑅1 ‘ suc 𝑦 ) )
36	35	ex	⊢ ( 𝑦 ∈ On → ( Tr ( 𝑅1 ‘ 𝑦 ) → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
37		triun	⊢ ( ∀ 𝑦 ∈ 𝑥 Tr ( 𝑅1 ‘ 𝑦 ) → Tr ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
38		r1limg	⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
39	38	ancoms	⊢ ( ( Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
40		treq	⊢ ( ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ) )
41	39 40	syl	⊢ ( ( Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ) )
42	37 41	imbitrrid	⊢ ( ( Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → ( ∀ 𝑦 ∈ 𝑥 Tr ( 𝑅1 ‘ 𝑦 ) → Tr ( 𝑅1 ‘ 𝑥 ) ) )
43	42	impancom	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑥 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ 𝑥 ) ) )
44		ndmfv	⊢ ( ¬ 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝑥 ) = ∅ )
45	44 10	syl	⊢ ( ¬ 𝑥 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ Tr ∅ ) )
46	21 45	mpbiri	⊢ ( ¬ 𝑥 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ 𝑥 ) )
47	43 46	pm2.61d1	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 Tr ( 𝑅1 ‘ 𝑦 ) ) → Tr ( 𝑅1 ‘ 𝑥 ) )
48	47	ex	⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 Tr ( 𝑅1 ‘ 𝑦 ) → Tr ( 𝑅1 ‘ 𝑥 ) ) )
49	11 14 17 20 21 36 48	tfinds	⊢ ( 𝐴 ∈ On → Tr ( 𝑅1 ‘ 𝐴 ) )
50	6 49	syl	⊢ ( 𝐴 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ 𝐴 ) )
51		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) = ∅ )
52		treq	⊢ ( ( 𝑅1 ‘ 𝐴 ) = ∅ → ( Tr ( 𝑅1 ‘ 𝐴 ) ↔ Tr ∅ ) )
53	51 52	syl	⊢ ( ¬ 𝐴 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ 𝐴 ) ↔ Tr ∅ ) )
54	21 53	mpbiri	⊢ ( ¬ 𝐴 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ 𝐴 ) )
55	50 54	pm2.61i	⊢ Tr ( 𝑅1 ‘ 𝐴 )