Metamath Proof Explorer


Theorem r1val1

Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of Enderton p. 202. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1val1 ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1𝐴 ) = 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐴 ∈ dom 𝑅1𝐴 = ∅ ) → 𝐴 = ∅ )
2 1 fveq2d ( ( 𝐴 ∈ dom 𝑅1𝐴 = ∅ ) → ( 𝑅1𝐴 ) = ( 𝑅1 ‘ ∅ ) )
3 r10 ( 𝑅1 ‘ ∅ ) = ∅
4 2 3 eqtrdi ( ( 𝐴 ∈ dom 𝑅1𝐴 = ∅ ) → ( 𝑅1𝐴 ) = ∅ )
5 0ss ∅ ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 )
6 5 a1i ( ( 𝐴 ∈ dom 𝑅1𝐴 = ∅ ) → ∅ ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
7 4 6 eqsstrd ( ( 𝐴 ∈ dom 𝑅1𝐴 = ∅ ) → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
8 nfv 𝑥 𝐴 ∈ dom 𝑅1
9 nfcv 𝑥 ( 𝑅1𝐴 )
10 nfiu1 𝑥 𝑥𝐴 𝒫 ( 𝑅1𝑥 )
11 9 10 nfss 𝑥 ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 )
12 simpr ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → 𝐴 = suc 𝑥 )
13 12 fveq2d ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → ( 𝑅1𝐴 ) = ( 𝑅1 ‘ suc 𝑥 ) )
14 eleq1 ( 𝐴 = suc 𝑥 → ( 𝐴 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1 ) )
15 14 biimpac ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → suc 𝑥 ∈ dom 𝑅1 )
16 r1funlim ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
17 16 simpri Lim dom 𝑅1
18 limsuc ( Lim dom 𝑅1 → ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1 ) )
19 17 18 ax-mp ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1 )
20 15 19 sylibr ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → 𝑥 ∈ dom 𝑅1 )
21 r1sucg ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1𝑥 ) )
22 20 21 syl ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1𝑥 ) )
23 13 22 eqtrd ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → ( 𝑅1𝐴 ) = 𝒫 ( 𝑅1𝑥 ) )
24 vex 𝑥 ∈ V
25 24 sucid 𝑥 ∈ suc 𝑥
26 25 12 eleqtrrid ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → 𝑥𝐴 )
27 ssiun2 ( 𝑥𝐴 → 𝒫 ( 𝑅1𝑥 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
28 26 27 syl ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → 𝒫 ( 𝑅1𝑥 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
29 23 28 eqsstrd ( ( 𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥 ) → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
30 29 ex ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 = suc 𝑥 → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ) )
31 30 a1d ( 𝐴 ∈ dom 𝑅1 → ( 𝑥 ∈ On → ( 𝐴 = suc 𝑥 → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ) ) )
32 8 11 31 rexlimd ( 𝐴 ∈ dom 𝑅1 → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ) )
33 32 imp ( ( 𝐴 ∈ dom 𝑅1 ∧ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
34 r1limg ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1𝐴 ) = 𝑥𝐴 ( 𝑅1𝑥 ) )
35 r1tr Tr ( 𝑅1𝑥 )
36 dftr4 ( Tr ( 𝑅1𝑥 ) ↔ ( 𝑅1𝑥 ) ⊆ 𝒫 ( 𝑅1𝑥 ) )
37 35 36 mpbi ( 𝑅1𝑥 ) ⊆ 𝒫 ( 𝑅1𝑥 )
38 37 a1i ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1𝑥 ) ⊆ 𝒫 ( 𝑅1𝑥 ) )
39 38 ralrimivw ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ∀ 𝑥𝐴 ( 𝑅1𝑥 ) ⊆ 𝒫 ( 𝑅1𝑥 ) )
40 ss2iun ( ∀ 𝑥𝐴 ( 𝑅1𝑥 ) ⊆ 𝒫 ( 𝑅1𝑥 ) → 𝑥𝐴 ( 𝑅1𝑥 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
41 39 40 syl ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → 𝑥𝐴 ( 𝑅1𝑥 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
42 34 41 eqsstrd ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
43 42 adantrl ( ( 𝐴 ∈ dom 𝑅1 ∧ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
44 limord ( Lim dom 𝑅1 → Ord dom 𝑅1 )
45 17 44 ax-mp Ord dom 𝑅1
46 ordsson ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
47 45 46 ax-mp dom 𝑅1 ⊆ On
48 47 sseli ( 𝐴 ∈ dom 𝑅1𝐴 ∈ On )
49 onzsl ( 𝐴 ∈ On ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
50 48 49 sylib ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
51 7 33 43 50 mpjao3dan ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1𝐴 ) ⊆ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )
52 ordtr1 ( Ord dom 𝑅1 → ( ( 𝑥𝐴𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
53 45 52 ax-mp ( ( 𝑥𝐴𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
54 53 ancoms ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → 𝑥 ∈ dom 𝑅1 )
55 54 21 syl ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1𝑥 ) )
56 simpr ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → 𝑥𝐴 )
57 ordelord ( ( Ord dom 𝑅1𝐴 ∈ dom 𝑅1 ) → Ord 𝐴 )
58 45 57 mpan ( 𝐴 ∈ dom 𝑅1 → Ord 𝐴 )
59 58 adantr ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → Ord 𝐴 )
60 ordelsuc ( ( 𝑥𝐴 ∧ Ord 𝐴 ) → ( 𝑥𝐴 ↔ suc 𝑥𝐴 ) )
61 56 59 60 syl2anc ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → ( 𝑥𝐴 ↔ suc 𝑥𝐴 ) )
62 56 61 mpbid ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → suc 𝑥𝐴 )
63 54 19 sylib ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → suc 𝑥 ∈ dom 𝑅1 )
64 simpl ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → 𝐴 ∈ dom 𝑅1 )
65 r1ord3g ( ( suc 𝑥 ∈ dom 𝑅1𝐴 ∈ dom 𝑅1 ) → ( suc 𝑥𝐴 → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1𝐴 ) ) )
66 63 64 65 syl2anc ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → ( suc 𝑥𝐴 → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1𝐴 ) ) )
67 62 66 mpd ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1𝐴 ) )
68 55 67 eqsstrrd ( ( 𝐴 ∈ dom 𝑅1𝑥𝐴 ) → 𝒫 ( 𝑅1𝑥 ) ⊆ ( 𝑅1𝐴 ) )
69 68 ralrimiva ( 𝐴 ∈ dom 𝑅1 → ∀ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ⊆ ( 𝑅1𝐴 ) )
70 iunss ( 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ⊆ ( 𝑅1𝐴 ) ↔ ∀ 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ⊆ ( 𝑅1𝐴 ) )
71 69 70 sylibr ( 𝐴 ∈ dom 𝑅1 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) ⊆ ( 𝑅1𝐴 ) )
72 51 71 eqssd ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1𝐴 ) = 𝑥𝐴 𝒫 ( 𝑅1𝑥 ) )