Step | Hyp | Ref
| Expression |
1 | | r1tr 8639 |
. . 3
⊢ Tr
(𝑅1‘𝐴) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → Tr
(𝑅1‘𝐴)) |
3 | | limelon 5788 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ On) |
4 | | r1fnon 8630 |
. . . . . . 7
⊢
𝑅1 Fn On |
5 | | fndm 5990 |
. . . . . . 7
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢ dom
𝑅1 = On |
7 | 3, 6 | syl6eleqr 2712 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ dom
𝑅1) |
8 | | onssr1 8694 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ⊆ (𝑅1‘𝐴)) |
10 | | 0ellim 5787 |
. . . . 5
⊢ (Lim
𝐴 → ∅ ∈
𝐴) |
11 | 10 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈ 𝐴) |
12 | 9, 11 | sseldd 3604 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈
(𝑅1‘𝐴)) |
13 | | ne0i 3921 |
. . 3
⊢ (∅
∈ (𝑅1‘𝐴) → (𝑅1‘𝐴) ≠ ∅) |
14 | 12, 13 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ≠ ∅) |
15 | | rankuni 8726 |
. . . . . 6
⊢
(rank‘∪ 𝑥) = ∪
(rank‘𝑥) |
16 | | rankon 8658 |
. . . . . . . . 9
⊢
(rank‘𝑥)
∈ On |
17 | | eloni 5733 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → Ord (rank‘𝑥)) |
18 | | orduniss 5821 |
. . . . . . . . 9
⊢ (Ord
(rank‘𝑥) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
19 | 16, 17, 18 | mp2b 10 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ⊆ (rank‘𝑥) |
20 | 19 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
21 | | rankr1ai 8661 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → (rank‘𝑥) ∈ 𝐴) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
23 | | onuni 6993 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → ∪ (rank‘𝑥) ∈ On) |
24 | 16, 23 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ∈ On |
25 | 3 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ On) |
26 | | ontr2 5772 |
. . . . . . . 8
⊢ ((∪ (rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
27 | 24, 25, 26 | sylancr 695 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
28 | 20, 22, 27 | mp2and 715 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ∈ 𝐴) |
29 | 15, 28 | syl5eqel 2705 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘∪ 𝑥)
∈ 𝐴) |
30 | | r1elwf 8659 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
31 | 30 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
32 | | uniwf 8682 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
33 | 31, 32 | sylib 208 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
34 | 7 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
35 | | rankr1ag 8665 |
. . . . . 6
⊢ ((∪ 𝑥
∈ ∪ (𝑅1 “ On) ∧
𝐴 ∈ dom
𝑅1) → (∪ 𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
36 | 33, 34, 35 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
37 | 29, 36 | mpbird 247 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ (𝑅1‘𝐴)) |
38 | | r1pwcl 8710 |
. . . . . 6
⊢ (Lim
𝐴 → (𝑥 ∈
(𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈ (𝑅1‘𝐴))) |
39 | 38 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑥 ∈ (𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
40 | 39 | biimpa 501 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝒫 𝑥 ∈
(𝑅1‘𝐴)) |
41 | 30 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
42 | | r1elwf 8659 |
. . . . . . . . 9
⊢ (𝑦 ∈
(𝑅1‘𝐴) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
43 | 42 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
44 | | rankprb 8714 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) →
(rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
45 | 41, 43, 44 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
46 | | limord 5784 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → Ord 𝐴) |
47 | 46 | ad3antlr 767 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → Ord 𝐴) |
48 | 22 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
49 | | rankr1ai 8661 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(𝑅1‘𝐴) → (rank‘𝑦) ∈ 𝐴) |
50 | 49 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑦) ∈ 𝐴) |
51 | | ordunel 7027 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (rank‘𝑥) ∈ 𝐴 ∧ (rank‘𝑦) ∈ 𝐴) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
52 | 47, 48, 50, 51 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
53 | | limsuc 7049 |
. . . . . . . . 9
⊢ (Lim
𝐴 →
(((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴 ↔ suc
((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴)) |
54 | 53 | ad3antlr 767 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴 ↔ suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴)) |
55 | 52, 54 | mpbid 222 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
56 | 45, 55 | eqeltrd 2701 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) ∈ 𝐴) |
57 | | prwf 8674 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
58 | 41, 43, 57 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
59 | 34 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
60 | | rankr1ag 8665 |
. . . . . . 7
⊢ (({𝑥, 𝑦} ∈ ∪
(𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) →
({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
61 | 58, 59, 60 | syl2anc 693 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
62 | 56, 61 | mpbird 247 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
63 | 62 | ralrimiva 2966 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
64 | 37, 40, 63 | 3jca 1242 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
65 | 64 | ralrimiva 2966 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∀𝑥 ∈ (𝑅1‘𝐴)(∪
𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
66 | | fvex 6201 |
. . 3
⊢
(𝑅1‘𝐴) ∈ V |
67 | | iswun 9526 |
. . 3
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))))) |
68 | 66, 67 | ax-mp 5 |
. 2
⊢
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)))) |
69 | 2, 14, 65, 68 | syl3anbrc 1246 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) |