| Step | Hyp | Ref
| Expression |
| 1 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
| 2 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑅1 |
| 3 | | nfiu1 5027 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
| 4 | 2, 3 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑥(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
| 5 | 1, 4 | dfssf 3974 |
. . . . 5
⊢ (𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
| 6 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 7 | 6 | rankid 9873 |
. . . . . 6
⊢ 𝑥 ∈
(𝑅1‘suc (rank‘𝑥)) |
| 8 | | ssiun2 5047 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → suc (rank‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
| 9 | | rankon 9835 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
| 10 | 9 | onsuci 7859 |
. . . . . . . . 9
⊢ suc
(rank‘𝑥) ∈
On |
| 11 | | rankr1b.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
| 12 | 10 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝐴 suc (rank‘𝑥) ∈ On |
| 13 | | iunon 8379 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) → ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On |
| 15 | | r1ord3 9822 |
. . . . . . . . 9
⊢ ((suc
(rank‘𝑥) ∈ On
∧ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) → (suc (rank‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) → (𝑅1‘suc
(rank‘𝑥)) ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
| 16 | 10, 14, 15 | mp2an 692 |
. . . . . . . 8
⊢ (suc
(rank‘𝑥) ⊆
∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) → (𝑅1‘suc
(rank‘𝑥)) ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
| 17 | 8, 16 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑅1‘suc
(rank‘𝑥)) ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
| 18 | 17 | sseld 3982 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝑅1‘suc
(rank‘𝑥)) →
𝑥 ∈
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
| 19 | 7, 18 | mpi 20 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
| 20 | 5, 19 | mpgbir 1799 |
. . . 4
⊢ 𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
| 21 | | fvex 6919 |
. . . . 5
⊢
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ∈ V |
| 22 | 21 | rankss 9889 |
. . . 4
⊢ (𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) → (rank‘𝐴) ⊆
(rank‘(𝑅1‘∪
𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
| 23 | 20, 22 | ax-mp 5 |
. . 3
⊢
(rank‘𝐴)
⊆ (rank‘(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
| 24 | | r1ord3 9822 |
. . . . . . 7
⊢
((∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On ∧ 𝑦 ∈ On) → (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦 → (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦))) |
| 25 | 14, 24 | mpan 690 |
. . . . . 6
⊢ (𝑦 ∈ On → (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦 → (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦))) |
| 26 | 25 | ss2rabi 4077 |
. . . . 5
⊢ {𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} ⊆ {𝑦 ∈ On ∣
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} |
| 27 | | intss 4969 |
. . . . 5
⊢ ({𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} ⊆ {𝑦 ∈ On ∣
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} → ∩ {𝑦
∈ On ∣ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} ⊆ ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦}) |
| 28 | 26, 27 | ax-mp 5 |
. . . 4
⊢ ∩ {𝑦
∈ On ∣ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} ⊆ ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} |
| 29 | | rankval2 9858 |
. . . . 5
⊢
((𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ∈ V →
(rank‘(𝑅1‘∪
𝑥 ∈ 𝐴 suc (rank‘𝑥))) = ∩ {𝑦 ∈ On ∣
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)}) |
| 30 | 21, 29 | ax-mp 5 |
. . . 4
⊢
(rank‘(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) = ∩ {𝑦 ∈ On ∣
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} |
| 31 | | intmin 4968 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On → ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
| 32 | 14, 31 | ax-mp 5 |
. . . . 5
⊢ ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
| 33 | 32 | eqcomi 2746 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) = ∩ {𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} |
| 34 | 28, 30, 33 | 3sstr4i 4035 |
. . 3
⊢
(rank‘(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) ⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
| 35 | 23, 34 | sstri 3993 |
. 2
⊢
(rank‘𝐴)
⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
| 36 | | iunss 5045 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴) ↔ ∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴)) |
| 37 | 11 | rankel 9879 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)) |
| 38 | | rankon 9835 |
. . . . 5
⊢
(rank‘𝐴)
∈ On |
| 39 | 9, 38 | onsucssi 7862 |
. . . 4
⊢
((rank‘𝑥)
∈ (rank‘𝐴)
↔ suc (rank‘𝑥)
⊆ (rank‘𝐴)) |
| 40 | 37, 39 | sylib 218 |
. . 3
⊢ (𝑥 ∈ 𝐴 → suc (rank‘𝑥) ⊆ (rank‘𝐴)) |
| 41 | 36, 40 | mprgbir 3068 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴) |
| 42 | 35, 41 | eqssi 4000 |
1
⊢
(rank‘𝐴) =
∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |