Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
2 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑅1 |
3 | | nfiu1 4486 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
4 | 2, 3 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑥(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
5 | 1, 4 | dfss2f 3559 |
. . . . 5
⊢ (𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
6 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
7 | 6 | rankid 8579 |
. . . . . 6
⊢ 𝑥 ∈
(𝑅1‘suc (rank‘𝑥)) |
8 | | ssiun2 4499 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → suc (rank‘𝑥) ⊆ ∪
𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
9 | | rankon 8541 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
10 | 9 | onsuci 6930 |
. . . . . . . . 9
⊢ suc
(rank‘𝑥) ∈
On |
11 | | rankr1b.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ V |
12 | 10 | rgenw 2908 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝐴 suc (rank‘𝑥) ∈ On |
13 | | iunon 7323 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) → ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) |
14 | 11, 12, 13 | mp2an 704 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On |
15 | | r1ord3 8528 |
. . . . . . . . 9
⊢ ((suc
(rank‘𝑥) ∈ On
∧ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On) → (suc (rank‘𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) → (𝑅1‘suc
(rank‘𝑥)) ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
16 | 10, 14, 15 | mp2an 704 |
. . . . . . . 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 3567 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝑅1‘suc
(rank‘𝑥)) →
𝑥 ∈
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
19 | 7, 18 | mpi 20 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
20 | 5, 19 | mpgbir 1717 |
. . . 4
⊢ 𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
21 | | fvex 6113 |
. . . . 5
⊢
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ∈ V |
22 | 21 | rankss 8595 |
. . . 4
⊢ (𝐴 ⊆
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) → (rank‘𝐴) ⊆
(rank‘(𝑅1‘∪
𝑥 ∈ 𝐴 suc (rank‘𝑥)))) |
23 | 20, 22 | ax-mp 5 |
. . 3
⊢
(rank‘𝐴)
⊆ (rank‘(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) |
24 | | r1ord3 8528 |
. . . . . . 7
⊢
((∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On ∧ 𝑦 ∈ On) → (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦 → (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦))) |
25 | 14, 24 | mpan 702 |
. . . . . 6
⊢ (𝑦 ∈ On → (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦 → (𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦))) |
26 | 25 | ss2rabi 3647 |
. . . . 5
⊢ {𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} ⊆ {𝑦 ∈ On ∣
(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) ⊆ (𝑅1‘𝑦)} |
27 | | intss 4433 |
. . . . 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 8564 |
. . . . 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 4432 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ∈ On → ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥)) |
32 | 14, 31 | ax-mp 5 |
. . . . 5
⊢ ∩ {𝑦
∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} = ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
33 | 32 | eqcomi 2619 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) = ∩ {𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ 𝑦} |
34 | 28, 30, 33 | 3sstr4i 3607 |
. . 3
⊢
(rank‘(𝑅1‘∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥))) ⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
35 | 23, 34 | sstri 3577 |
. 2
⊢
(rank‘𝐴)
⊆ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |
36 | | iunss 4497 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴) ↔ ∀𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴)) |
37 | 11 | rankel 8585 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)) |
38 | | rankon 8541 |
. . . . 5
⊢
(rank‘𝐴)
∈ On |
39 | 9, 38 | onsucssi 6933 |
. . . 4
⊢
((rank‘𝑥)
∈ (rank‘𝐴)
↔ suc (rank‘𝑥)
⊆ (rank‘𝐴)) |
40 | 37, 39 | sylib 207 |
. . 3
⊢ (𝑥 ∈ 𝐴 → suc (rank‘𝑥) ⊆ (rank‘𝐴)) |
41 | 36, 40 | mprgbir 2911 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) ⊆ (rank‘𝐴) |
42 | 35, 41 | eqssi 3584 |
1
⊢
(rank‘𝐴) =
∪ 𝑥 ∈ 𝐴 suc (rank‘𝑥) |