| Step | Hyp | Ref
| Expression |
| 1 | | uniwf 9859 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
| 2 | | rankval3b 9866 |
. . . 4
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
| 3 | 1, 2 | sylbi 217 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
| 4 | | eleq2 2830 |
. . . . . 6
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → ((rank‘𝑦) ∈ 𝑧 ↔ (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
| 5 | 4 | ralbidv 3178 |
. . . . 5
⊢ (𝑧 = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
| 6 | | iuneq1 5008 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ∪
𝑥 ∈ 𝑦 (rank‘𝑥) = ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 7 | 6 | eleq1d 2826 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∪
𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On ↔ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On)) |
| 8 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 9 | | rankon 9835 |
. . . . . . . 8
⊢
(rank‘𝑥)
∈ On |
| 10 | 9 | rgenw 3065 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑦 (rank‘𝑥) ∈ On |
| 11 | | iunon 8379 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ ∀𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) → ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On) |
| 12 | 8, 10, 11 | mp2an 692 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝑦 (rank‘𝑥) ∈ On |
| 13 | 7, 12 | vtoclg 3554 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ On) |
| 14 | | eluni2 4911 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑦 ∈ 𝑥) |
| 15 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ∈ ∪ (𝑅1 “ On) |
| 16 | | nfiu1 5027 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (rank‘𝑥) |
| 17 | 16 | nfel2 2924 |
. . . . . . . 8
⊢
Ⅎ𝑥(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥) |
| 18 | | r1elssi 9845 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
| 19 | 18 | sseld 3982 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪
(𝑅1 “ On))) |
| 20 | | rankelb 9864 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥))) |
| 21 | 19, 20 | syl6 35 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ (rank‘𝑥)))) |
| 22 | | ssiun2 5047 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 23 | 22 | sseld 3982 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ((rank‘𝑦) ∈ (rank‘𝑥) → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
| 24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → ((rank‘𝑦) ∈ (rank‘𝑥) → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)))) |
| 25 | 21, 24 | syldd 72 |
. . . . . . . 8
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)))) |
| 26 | 15, 17, 25 | rexlimd 3266 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → (rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥))) |
| 27 | 14, 26 | biimtrid 242 |
. . . . . 6
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ ∪ 𝐴
→ (rank‘𝑦)
∈ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥))) |
| 28 | 27 | ralrimiv 3145 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 29 | 5, 13, 28 | elrabd 3694 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧}) |
| 30 | | intss1 4963 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} → ∩ {𝑧 ∈ On ∣ ∀𝑦 ∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 31 | 29, 30 | syl 17 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑧
∈ On ∣ ∀𝑦
∈ ∪ 𝐴(rank‘𝑦) ∈ 𝑧} ⊆ ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 32 | 3, 31 | eqsstrd 4018 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) ⊆ ∪ 𝑥 ∈ 𝐴 (rank‘𝑥)) |
| 33 | 1 | biimpi 216 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝐴
∈ ∪ (𝑅1 “
On)) |
| 34 | | elssuni 4937 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) |
| 35 | | rankssb 9888 |
. . . . 5
⊢ (∪ 𝐴
∈ ∪ (𝑅1 “ On) →
(𝑥 ⊆ ∪ 𝐴
→ (rank‘𝑥)
⊆ (rank‘∪ 𝐴))) |
| 36 | 33, 34, 35 | syl2im 40 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘∪ 𝐴))) |
| 37 | 36 | ralrimiv 3145 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
| 38 | | iunss 5045 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)
↔ ∀𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
| 39 | 37, 38 | sylibr 234 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘∪ 𝐴)) |
| 40 | 32, 39 | eqssd 4001 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ 𝐴) = ∪
𝑥 ∈ 𝐴 (rank‘𝑥)) |