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 r1dmlim ⊢ Lim dom 𝑅1
17 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1 ) )
18 16 17 ax-mp ⊢ ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1 )
19 15 18 sylibr ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → 𝑥 ∈ dom 𝑅1 )
20 r1sucg ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
22 13 21 eqtrd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → ( 𝑅1 ‘ 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
23 vex ⊢ 𝑥 ∈ V
24 23 sucid ⊢ 𝑥 ∈ suc 𝑥
25 24 12 eleqtrrid ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → 𝑥 ∈ 𝐴 )
26 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
27 25 26 syl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
28 22 27 eqsstrd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐴 = suc 𝑥 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
29 28 ex ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 = suc 𝑥 → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
30 29 a1d ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑥 ∈ On → ( 𝐴 = suc 𝑥 → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ) ) )
31 8 11 30 rexlimd ⊢ ( 𝐴 ∈ dom 𝑅1 → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
32 31 imp ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
33 r1limg ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
34 r1tr ⊢ Tr ( 𝑅1 ‘ 𝑥 )
35 dftr4 ⊢ ( Tr ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝑥 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
36 34 35 mpbi ⊢ ( 𝑅1 ‘ 𝑥 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑥 )
37 36 a1i ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
38 37 ralrimivw ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
39 ss2iun ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑥 ) → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
40 38 39 syl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
41 33 40 eqsstrd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
42 41 adantrl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
43 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
44 16 43 ax-mp ⊢ Ord dom 𝑅1
45 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
46 44 45 ax-mp ⊢ dom 𝑅1 ⊆ On
47 46 sseli ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On )
48 onzsl ⊢ ( 𝐴 ∈ On ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
49 47 48 sylib ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ ( 𝐴 ∈ V ∧ Lim 𝐴 ) ) )
50 7 32 42 49 mpjao3dan ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )
51 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
52 44 51 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
53 52 ancoms ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
54 53 20 syl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
55 simpr ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
56 ordelord ⊢ ( ( Ord dom 𝑅1 ∧ 𝐴 ∈ dom 𝑅1 ) → Ord 𝐴 )
57 44 56 mpan ⊢ ( 𝐴 ∈ dom 𝑅1 → Ord 𝐴 )
58 57 adantr ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝐴 )
59 ordelsuc ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Ord 𝐴 ) → ( 𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴 ) )
60 55 58 59 syl2anc ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↔ suc 𝑥 ⊆ 𝐴 ) )
61 55 60 mpbid ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → suc 𝑥 ⊆ 𝐴 )
62 53 18 sylib ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → suc 𝑥 ∈ dom 𝑅1 )
63 simpl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
64 r1ord3g ⊢ ( ( suc 𝑥 ∈ dom 𝑅1 ∧ 𝐴 ∈ dom 𝑅1 ) → ( suc 𝑥 ⊆ 𝐴 → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
65 62 63 64 syl2anc ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( suc 𝑥 ⊆ 𝐴 → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
66 61 65 mpd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ suc 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
67 54 66 eqsstrrd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
68 67 ralrimiva ⊢ ( 𝐴 ∈ dom 𝑅1 → ∀ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
69 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
70 68 69 sylibr ⊢ ( 𝐴 ∈ dom 𝑅1 → ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
71 50 70 eqssd ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 𝒫 ( 𝑅1 ‘ 𝑥 ) )