Step | Hyp | Ref
| Expression |
1 | | r1tr 9392 |
. . 3
⊢ Tr
(𝑅1‘𝐴) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → Tr
(𝑅1‘𝐴)) |
3 | | limelon 6276 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ On) |
4 | | r1fnon 9383 |
. . . . . . 7
⊢
𝑅1 Fn On |
5 | 4 | fndmi 6482 |
. . . . . 6
⊢ dom
𝑅1 = On |
6 | 3, 5 | eleqtrrdi 2849 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ∈ dom
𝑅1) |
7 | | onssr1 9447 |
. . . . 5
⊢ (𝐴 ∈ dom
𝑅1 → 𝐴 ⊆ (𝑅1‘𝐴)) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ⊆ (𝑅1‘𝐴)) |
9 | | 0ellim 6275 |
. . . . 5
⊢ (Lim
𝐴 → ∅ ∈
𝐴) |
10 | 9 | adantl 485 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈ 𝐴) |
11 | 8, 10 | sseldd 3902 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∅ ∈
(𝑅1‘𝐴)) |
12 | 11 | ne0d 4250 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ≠ ∅) |
13 | | rankuni 9479 |
. . . . . 6
⊢
(rank‘∪ 𝑥) = ∪
(rank‘𝑥) |
14 | | rankon 9411 |
. . . . . . . . 9
⊢
(rank‘𝑥)
∈ On |
15 | | eloni 6223 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → Ord (rank‘𝑥)) |
16 | | orduniss 6307 |
. . . . . . . . 9
⊢ (Ord
(rank‘𝑥) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
17 | 14, 15, 16 | mp2b 10 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ⊆ (rank‘𝑥) |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ⊆ (rank‘𝑥)) |
19 | | rankr1ai 9414 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → (rank‘𝑥) ∈ 𝐴) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
21 | | onuni 7572 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ On → ∪ (rank‘𝑥) ∈ On) |
22 | 14, 21 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ (rank‘𝑥) ∈ On |
23 | 3 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ On) |
24 | | ontr2 6260 |
. . . . . . . 8
⊢ ((∪ (rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
25 | 22, 23, 24 | sylancr 590 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ((∪ (rank‘𝑥) ⊆ (rank‘𝑥) ∧ (rank‘𝑥) ∈ 𝐴) → ∪
(rank‘𝑥) ∈ 𝐴)) |
26 | 18, 20, 25 | mp2and 699 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ (rank‘𝑥) ∈ 𝐴) |
27 | 13, 26 | eqeltrid 2842 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (rank‘∪ 𝑥)
∈ 𝐴) |
28 | | r1elwf 9412 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑅1‘𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
29 | 28 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
30 | | uniwf 9435 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
31 | 29, 30 | sylib 221 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ ∪ (𝑅1 “
On)) |
32 | 6 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
33 | | rankr1ag 9418 |
. . . . . 6
⊢ ((∪ 𝑥
∈ ∪ (𝑅1 “ On) ∧
𝐴 ∈ dom
𝑅1) → (∪ 𝑥 ∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
34 | 31, 32, 33 | syl2anc 587 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ↔ (rank‘∪ 𝑥)
∈ 𝐴)) |
35 | 27, 34 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∪ 𝑥
∈ (𝑅1‘𝐴)) |
36 | | r1pwcl 9463 |
. . . . . 6
⊢ (Lim
𝐴 → (𝑥 ∈
(𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈ (𝑅1‘𝐴))) |
37 | 36 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑥 ∈ (𝑅1‘𝐴) ↔ 𝒫 𝑥 ∈
(𝑅1‘𝐴))) |
38 | 37 | biimpa 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → 𝒫 𝑥 ∈
(𝑅1‘𝐴)) |
39 | 28 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
40 | | r1elwf 9412 |
. . . . . . . . 9
⊢ (𝑦 ∈
(𝑅1‘𝐴) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
41 | 40 | adantl 485 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
42 | | rankprb 9467 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) →
(rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
43 | 39, 41, 42 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) = suc ((rank‘𝑥) ∪ (rank‘𝑦))) |
44 | | limord 6272 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → Ord 𝐴) |
45 | 44 | ad3antlr 731 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → Ord 𝐴) |
46 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑥) ∈ 𝐴) |
47 | | rankr1ai 9414 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(𝑅1‘𝐴) → (rank‘𝑦) ∈ 𝐴) |
48 | 47 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘𝑦) ∈ 𝐴) |
49 | | ordunel 7606 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ (rank‘𝑥) ∈ 𝐴 ∧ (rank‘𝑦) ∈ 𝐴) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
50 | 45, 46, 48, 49 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
51 | | limsuc 7628 |
. . . . . . . . 9
⊢ (Lim
𝐴 →
(((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴 ↔ suc
((rank‘𝑥) ∪
(rank‘𝑦)) ∈
𝐴)) |
52 | 51 | ad3antlr 731 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴 ↔ suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴)) |
53 | 50, 52 | mpbid 235 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → suc ((rank‘𝑥) ∪ (rank‘𝑦)) ∈ 𝐴) |
54 | 43, 53 | eqeltrd 2838 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → (rank‘{𝑥, 𝑦}) ∈ 𝐴) |
55 | | prwf 9427 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ (𝑅1 “ On) ∧ 𝑦 ∈ ∪ (𝑅1 “ On)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
56 | 39, 41, 55 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ ∪
(𝑅1 “ On)) |
57 | 32 | adantr 484 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → 𝐴 ∈ dom
𝑅1) |
58 | | rankr1ag 9418 |
. . . . . . 7
⊢ (({𝑥, 𝑦} ∈ ∪
(𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) →
({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
59 | 56, 57, 58 | syl2anc 587 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → ({𝑥, 𝑦} ∈ (𝑅1‘𝐴) ↔ (rank‘{𝑥, 𝑦}) ∈ 𝐴)) |
60 | 54, 59 | mpbird 260 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) ∧ 𝑦 ∈ (𝑅1‘𝐴)) → {𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
61 | 60 | ralrimiva 3105 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)) |
62 | 35, 38, 61 | 3jca 1130 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ Lim 𝐴) ∧ 𝑥 ∈ (𝑅1‘𝐴)) → (∪ 𝑥
∈ (𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
63 | 62 | ralrimiva 3105 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → ∀𝑥 ∈ (𝑅1‘𝐴)(∪
𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))) |
64 | | fvex 6730 |
. . 3
⊢
(𝑅1‘𝐴) ∈ V |
65 | | iswun 10318 |
. . 3
⊢
((𝑅1‘𝐴) ∈ V →
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴))))) |
66 | 64, 65 | ax-mp 5 |
. 2
⊢
((𝑅1‘𝐴) ∈ WUni ↔ (Tr
(𝑅1‘𝐴) ∧ (𝑅1‘𝐴) ≠ ∅ ∧
∀𝑥 ∈
(𝑅1‘𝐴)(∪ 𝑥 ∈
(𝑅1‘𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1‘𝐴) ∧ ∀𝑦 ∈
(𝑅1‘𝐴){𝑥, 𝑦} ∈ (𝑅1‘𝐴)))) |
67 | 2, 12, 63, 66 | syl3anbrc 1345 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) |