Step | Hyp | Ref
| Expression |
1 | | uniwf 8682 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
2 | | rankval3b 8689 |
. . . 4
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
3 | 1, 2 | sylbi 207 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
4 | | iuneq1 4534 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ∪
𝑥 ∈ 𝑦 (rank‘𝑥) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
5 | 4 | eleq1d 2686 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∪
𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On ↔ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On)) |
6 | | vex 3203 |
. . . . . . 7
⊢ 𝑦 ∈ V |
7 | | rankon 8658 |
. . . . . . . 8
⊢
(rank‘𝑥)
∈ On |
8 | 7 | rgenw 2924 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑦 (rank‘𝑥) ∈ On |
9 | | iunon 7436 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ ∀𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) → ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) |
10 | 6, 8, 9 | mp2an 708 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On |
11 | 5, 10 | vtoclg 3266 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On) |
12 | | eluni2 4440 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑦 ∈ 𝑥) |
13 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ∈ ∪ (𝑅1 “ On) |
14 | | nfiu1 4550 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (rank‘𝑥) |
15 | 14 | nfel2 2781 |
. . . . . . . 8
⊢
Ⅎ𝑥(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥) |
16 | | r1elssi 8668 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
17 | 16 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
(𝑅1 “ On))) |
18 | | rankelb 8687 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥))) |
19 | 17, 18 | syl6 35 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥)))) |
20 | | ssiun2 4563 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
21 | 20 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ((rank‘𝑦) ∈ (rank‘𝑥) → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → ((rank‘𝑦) ∈ (rank‘𝑥) → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)))) |
23 | 19, 22 | syldd 72 |
. . . . . . . 8
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)))) |
24 | 13, 15, 23 | rexlimd 3026 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
25 | 12, 24 | syl5bi 232 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ ∪ 𝐴
→ (rank‘𝑦)
∈ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥))) |
26 | 25 | ralrimiv 2965 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
27 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → ((rank‘𝑦) ∈ 𝑧 ↔ (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
28 | 27 | ralbidv 2986 |
. . . . . 6
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
29 | 28 | elrab 3363 |
. . . . 5
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ↔ (∪
𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On ∧ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
30 | 11, 26, 29 | sylanbrc 698 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
31 | | intss1 4492 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} → ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
32 | 30, 31 | syl 17 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑧
∈ On ∣ ∀𝑦
∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
33 | 3, 32 | eqsstrd 3639 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
34 | 1 | biimpi 206 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
35 | | elssuni 4467 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) |
36 | | rankssb 8711 |
. . . . 5
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(𝑥 ⊆ ∪ 𝐴
→ (rank‘𝑥)
⊆ (rank‘∪ 𝐴))) |
37 | 34, 35, 36 | syl2im 40 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘∪ 𝐴))) |
38 | 37 | ralrimiv 2965 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
39 | | iunss 4561 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)
↔ ∀𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
40 | 38, 39 | sylibr 224 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
41 | 33, 40 | eqssd 3620 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |