Step | Hyp | Ref
| Expression |
1 | | r1tr 8999 |
. . 3
⊢ Tr
(𝑅1‘𝐴) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → Tr
(𝑅1‘𝐴)) |
3 | | limelon 6092 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ On) |
4 | | r1fnon 8990 |
. . . . . . 7
⊢
𝑅1 Fn On |
5 | | fndm 6288 |
. . . . . . 7
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
7 | 3, 6 | syl6eleqr 2877 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ dom
𝑅1) |
8 | | onssr1 9054 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ⊆ (𝑅1‘𝐴)) |
10 | | 0ellim 6091 |
. . . . 5
⊢ (Lim
𝐴 → ∅ ∈
𝐴) |
11 | 10 | adantl 474 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈ 𝐴) |
12 | 9, 11 | sseldd 3859 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈
(𝑅1‘𝐴)) |
13 | 12 | ne0d 4187 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ≠ ∅) |
14 | | rankuni 9086 |
. . . . . 6
⊢
(rank‘∪ 𝑥) = ∪
(rank‘𝑥) |
15 | | rankon 9018 |
. . . . . . . . 9
⊢
(rank‘𝑥)
∈ On |
16 | | eloni 6039 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → Ord (rank‘𝑥)) |
17 | | orduniss 6123 |
. . . . . . . . 9
⊢ (Ord
(rank‘𝑥) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
18 | 15, 16, 17 | mp2b 10 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ⊆ (rank‘𝑥) |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
20 | | rankr1ai 9021 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → (rank‘𝑥) ∈ 𝐴) |
21 | 20 | adantl 474 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
22 | | onuni 7324 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → ∪ (rank‘𝑥) ∈ On) |
23 | 15, 22 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ∈ On |
24 | 3 | adantr 473 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ On) |
25 | | ontr2 6076 |
. . . . . . . 8
⊢ ((∪ (rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
26 | 23, 24, 25 | sylancr 578 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
27 | 19, 21, 26 | mp2and 686 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ∈ 𝐴) |
28 | 14, 27 | syl5eqel 2870 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘∪ 𝑥)
∈ 𝐴) |
29 | | r1elwf 9019 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
30 | 29 | adantl 474 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
31 | | uniwf 9042 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
32 | 30, 31 | sylib 210 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
33 | 7 | adantr 473 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
34 | | rankr1ag 9025 |
. . . . . 6
⊢ ((∪ 𝑥
∈ ∪ (𝑅1 “ On) ∧
𝐴 ∈ dom
𝑅1) → (∪ 𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
35 | 32, 33, 34 | syl2anc 576 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
36 | 28, 35 | mpbird 249 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ (𝑅1‘𝐴)) |
37 | | r1pwcl 9070 |
. . . . . 6
⊢ (Lim
𝐴 → (𝑥 ∈
(𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈ (𝑅1‘𝐴))) |
38 | 37 | adantl 474 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑥 ∈ (𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
39 | 38 | biimpa 469 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝒫 𝑥 ∈
(𝑅1‘𝐴)) |
40 | 29 | ad2antlr 714 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
41 | | r1elwf 9019 |
. . . . . . . . 9
⊢ (𝑦 ∈
(𝑅1‘𝐴) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
42 | 41 | adantl 474 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
43 | | rankprb 9074 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) →
(rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
44 | 40, 42, 43 | syl2anc 576 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
45 | | limord 6088 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → Ord 𝐴) |
46 | 45 | ad3antlr 718 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → Ord 𝐴) |
47 | 21 | adantr 473 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
48 | | rankr1ai 9021 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(𝑅1‘𝐴) → (rank‘𝑦) ∈ 𝐴) |
49 | 48 | adantl 474 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑦) ∈ 𝐴) |
50 | | ordunel 7358 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (rank‘𝑥) ∈ 𝐴 ∧ (rank‘𝑦) ∈ 𝐴) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
51 | 46, 47, 49, 50 | syl3anc 1351 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
52 | | limsuc 7380 |
. . . . . . . . 9
⊢ (Lim
𝐴 →
(((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴 ↔ suc
((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴)) |
53 | 52 | ad3antlr 718 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴 ↔ suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴)) |
54 | 51, 53 | mpbid 224 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
55 | 44, 54 | eqeltrd 2866 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) ∈ 𝐴) |
56 | | prwf 9034 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
57 | 40, 42, 56 | syl2anc 576 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
58 | 33 | adantr 473 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
59 | | rankr1ag 9025 |
. . . . . . 7
⊢ (({𝑥, 𝑦} ∈ ∪
(𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) →
({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
60 | 57, 58, 59 | syl2anc 576 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
61 | 55, 60 | mpbird 249 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
62 | 61 | ralrimiva 3132 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
63 | 36, 39, 62 | 3jca 1108 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
64 | 63 | ralrimiva 3132 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∀𝑥 ∈ (𝑅1‘𝐴)(∪
𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
65 | | fvex 6512 |
. . 3
⊢
(𝑅1‘𝐴) ∈ V |
66 | | iswun 9924 |
. . 3
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))))) |
67 | 65, 66 | ax-mp 5 |
. 2
⊢
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)))) |
68 | 2, 13, 64, 67 | syl3anbrc 1323 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) |