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

Proof

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