Theorem r1tr 9795

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.)

Assertion

Ref	Expression
r1tr	⊢ Tr (𝑅1‘𝐴)

Proof of Theorem r1tr

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		r1funlim 9785	. . . . . 6 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . 5 ⊢ Lim dom 𝑅1
3		limord 6418	. . . . 5 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4		ordsson 7782	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
5	2, 3, 4	mp2b 10	. . . 4 ⊢ dom 𝑅1 ⊆ On
6	5	sseli 3959	. . 3 ⊢ (𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On)
7		fveq2 6881	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = (𝑅1‘∅))
8		r10 9787	. . . . . 6 ⊢ (𝑅1‘∅) = ∅
9	7, 8	eqtrdi 2787	. . . . 5 ⊢ (𝑥 = ∅ → (𝑅1‘𝑥) = ∅)
10		treq 5242	. . . . 5 ⊢ ((𝑅1‘𝑥) = ∅ → (Tr (𝑅1‘𝑥) ↔ Tr ∅))
11	9, 10	syl 17	. . . 4 ⊢ (𝑥 = ∅ → (Tr (𝑅1‘𝑥) ↔ Tr ∅))
12		fveq2 6881	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) = (𝑅1‘𝑦))
13		treq 5242	. . . . 5 ⊢ ((𝑅1‘𝑥) = (𝑅1‘𝑦) → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘𝑦)))
14	12, 13	syl 17	. . . 4 ⊢ (𝑥 = 𝑦 → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘𝑦)))
15		fveq2 6881	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) = (𝑅1‘suc 𝑦))
16		treq 5242	. . . . 5 ⊢ ((𝑅1‘𝑥) = (𝑅1‘suc 𝑦) → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘suc 𝑦)))
17	15, 16	syl 17	. . . 4 ⊢ (𝑥 = suc 𝑦 → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘suc 𝑦)))
18		fveq2 6881	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑅1‘𝑥) = (𝑅1‘𝐴))
19		treq 5242	. . . . 5 ⊢ ((𝑅1‘𝑥) = (𝑅1‘𝐴) → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘𝐴)))
20	18, 19	syl 17	. . . 4 ⊢ (𝑥 = 𝐴 → (Tr (𝑅1‘𝑥) ↔ Tr (𝑅1‘𝐴)))
21		tr0 5247	. . . 4 ⊢ Tr ∅
22		limsuc 7849	. . . . . . . 8 ⊢ (Lim dom 𝑅1 → (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1))
23	2, 22	ax-mp 5	. . . . . . 7 ⊢ (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1)
24		simpr 484	. . . . . . . . 9 ⊢ ((𝑦 ∈ On ∧ Tr (𝑅1‘𝑦)) → Tr (𝑅1‘𝑦))
25		pwtr 5432	. . . . . . . . 9 ⊢ (Tr (𝑅1‘𝑦) ↔ Tr 𝒫 (𝑅1‘𝑦))
26	24, 25	sylib 218	. . . . . . . 8 ⊢ ((𝑦 ∈ On ∧ Tr (𝑅1‘𝑦)) → Tr 𝒫 (𝑅1‘𝑦))
27		r1sucg 9788	. . . . . . . . 9 ⊢ (𝑦 ∈ dom 𝑅1 → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦))
28		treq 5242	. . . . . . . . 9 ⊢ ((𝑅1‘suc 𝑦) = 𝒫 (𝑅1‘𝑦) → (Tr (𝑅1‘suc 𝑦) ↔ Tr 𝒫 (𝑅1‘𝑦)))
29	27, 28	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ dom 𝑅1 → (Tr (𝑅1‘suc 𝑦) ↔ Tr 𝒫 (𝑅1‘𝑦)))
30	26, 29	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ Tr (𝑅1‘𝑦)) → (𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦)))
31	23, 30	biimtrrid 243	. . . . . 6 ⊢ ((𝑦 ∈ On ∧ Tr (𝑅1‘𝑦)) → (suc 𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦)))
32		ndmfv 6916	. . . . . . . 8 ⊢ (¬ suc 𝑦 ∈ dom 𝑅1 → (𝑅1‘suc 𝑦) = ∅)
33		treq 5242	. . . . . . . 8 ⊢ ((𝑅1‘suc 𝑦) = ∅ → (Tr (𝑅1‘suc 𝑦) ↔ Tr ∅))
34	32, 33	syl 17	. . . . . . 7 ⊢ (¬ suc 𝑦 ∈ dom 𝑅1 → (Tr (𝑅1‘suc 𝑦) ↔ Tr ∅))
35	21, 34	mpbiri 258	. . . . . 6 ⊢ (¬ suc 𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦))
36	31, 35	pm2.61d1 180	. . . . 5 ⊢ ((𝑦 ∈ On ∧ Tr (𝑅1‘𝑦)) → Tr (𝑅1‘suc 𝑦))
37	36	ex 412	. . . 4 ⊢ (𝑦 ∈ On → (Tr (𝑅1‘𝑦) → Tr (𝑅1‘suc 𝑦)))
38		triun 5249	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 Tr (𝑅1‘𝑦) → Tr ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦))
39		r1limg 9790	. . . . . . . . . 10 ⊢ ((𝑥 ∈ dom 𝑅1 ∧ Lim 𝑥) → (𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦))
40	39	ancoms 458	. . . . . . . . 9 ⊢ ((Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1) → (𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦))
41		treq 5242	. . . . . . . . 9 ⊢ ((𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦) → (Tr (𝑅1‘𝑥) ↔ Tr ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)))
42	40, 41	syl 17	. . . . . . . 8 ⊢ ((Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1) → (Tr (𝑅1‘𝑥) ↔ Tr ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)))
43	38, 42	imbitrrid 246	. . . . . . 7 ⊢ ((Lim 𝑥 ∧ 𝑥 ∈ dom 𝑅1) → (∀𝑦 ∈ 𝑥 Tr (𝑅1‘𝑦) → Tr (𝑅1‘𝑥)))
44	43	impancom 451	. . . . . 6 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr (𝑅1‘𝑦)) → (𝑥 ∈ dom 𝑅1 → Tr (𝑅1‘𝑥)))
45		ndmfv 6916	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ dom 𝑅1 → (𝑅1‘𝑥) = ∅)
46	45, 10	syl 17	. . . . . . 7 ⊢ (¬ 𝑥 ∈ dom 𝑅1 → (Tr (𝑅1‘𝑥) ↔ Tr ∅))
47	21, 46	mpbiri 258	. . . . . 6 ⊢ (¬ 𝑥 ∈ dom 𝑅1 → Tr (𝑅1‘𝑥))
48	44, 47	pm2.61d1 180	. . . . 5 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr (𝑅1‘𝑦)) → Tr (𝑅1‘𝑥))
49	48	ex 412	. . . 4 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 Tr (𝑅1‘𝑦) → Tr (𝑅1‘𝑥)))
50	11, 14, 17, 20, 21, 37, 49	tfinds 7860	. . 3 ⊢ (𝐴 ∈ On → Tr (𝑅1‘𝐴))
51	6, 50	syl 17	. 2 ⊢ (𝐴 ∈ dom 𝑅1 → Tr (𝑅1‘𝐴))
52		ndmfv 6916	. . . 4 ⊢ (¬ 𝐴 ∈ dom 𝑅1 → (𝑅1‘𝐴) = ∅)
53		treq 5242	. . . 4 ⊢ ((𝑅1‘𝐴) = ∅ → (Tr (𝑅1‘𝐴) ↔ Tr ∅))
54	52, 53	syl 17	. . 3 ⊢ (¬ 𝐴 ∈ dom 𝑅1 → (Tr (𝑅1‘𝐴) ↔ Tr ∅))
55	21, 54	mpbiri 258	. 2 ⊢ (¬ 𝐴 ∈ dom 𝑅1 → Tr (𝑅1‘𝐴))
56	51, 55	pm2.61i 182	1 ⊢ Tr (𝑅1‘𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  ∪ ciun 4972  Tr wtr 5234  dom cdm 5659  Ord word 6356  Oncon0 6357  Lim wlim 6358  suc csuc 6359  Fun wfun 6530  ‘cfv 6536  𝑅₁cr1 9781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-r1 9783

This theorem is referenced by:  r1tr2  9796  r1ordg  9797  r1ord3g  9798  r1ord2  9800  r1sssuc  9802  r1pwss  9803  r1val1  9805  rankwflemb  9812  r1elwf  9815  r1elssi  9824  uniwf  9838  tcrank  9903  ackbij2lem3  10259  r1limwun  10755  tskr1om2  10787  inagrud  44295