Step | Hyp | Ref
| Expression |
1 | | uniwf 8846 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
2 | | rankval3b 8853 |
. . . 4
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
3 | 1, 2 | sylbi 207 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
4 | | iuneq1 4668 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ∪
𝑥 ∈ 𝑦 (rank‘𝑥) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
5 | 4 | eleq1d 2835 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∪
𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On ↔ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On)) |
6 | | vex 3354 |
. . . . . . 7
⊢ 𝑦 ∈ V |
7 | | rankon 8822 |
. . . . . . . 8
⊢
(rank‘𝑥)
∈ On |
8 | 7 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑦 (rank‘𝑥) ∈ On |
9 | | iunon 7589 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ ∀𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) → ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) |
10 | 6, 8, 9 | mp2an 672 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On |
11 | 5, 10 | vtoclg 3417 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On) |
12 | | eluni2 4578 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑦 ∈ 𝑥) |
13 | | nfv 1995 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ∈ ∪ (𝑅1 “ On) |
14 | | nfiu1 4684 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (rank‘𝑥) |
15 | 14 | nfel2 2930 |
. . . . . . . 8
⊢
Ⅎ𝑥(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥) |
16 | | r1elssi 8832 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
17 | 16 | sseld 3751 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
(𝑅1 “ On))) |
18 | | rankelb 8851 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥))) |
19 | 17, 18 | syl6 35 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥)))) |
20 | | ssiun2 4697 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
21 | 20 | sseld 3751 |
. . . . . . . . . 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 3174 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
25 | 12, 24 | syl5bi 232 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ ∪ 𝐴
→ (rank‘𝑦)
∈ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥))) |
26 | 25 | ralrimiv 3114 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
27 | | eleq2 2839 |
. . . . . . 7
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → ((rank‘𝑦) ∈ 𝑧 ↔ (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
28 | 27 | ralbidv 3135 |
. . . . . 6
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
29 | 28 | elrab 3515 |
. . . . 5
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ↔ (∪
𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On ∧ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
30 | 11, 26, 29 | sylanbrc 572 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
31 | | intss1 4626 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} → ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
32 | 30, 31 | syl 17 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑧
∈ On ∣ ∀𝑦
∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
33 | 3, 32 | eqsstrd 3788 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
34 | 1 | biimpi 206 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
35 | | elssuni 4603 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) |
36 | | rankssb 8875 |
. . . . 5
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(𝑥 ⊆ ∪ 𝐴
→ (rank‘𝑥)
⊆ (rank‘∪ 𝐴))) |
37 | 34, 35, 36 | syl2im 40 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘∪ 𝐴))) |
38 | 37 | ralrimiv 3114 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
39 | | iunss 4695 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)
↔ ∀𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
40 | 38, 39 | sylibr 224 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
41 | 33, 40 | eqssd 3769 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |