Proof of Theorem scott0
| Step | Hyp | Ref
| Expression |
| 1 | | rabeq 3451 |
. . 3
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}) |
| 2 | | rab0 4386 |
. . 3
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ |
| 3 | 1, 2 | eqtrdi 2793 |
. 2
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |
| 4 | | n0 4353 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
| 5 | | nfre1 3285 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(rank‘𝑥) =
(rank‘𝑥) |
| 7 | | rspe 3249 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
| 8 | 6, 7 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
| 9 | 5, 8 | exlimi 2217 |
. . . . . . . 8
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
| 10 | 4, 9 | sylbi 217 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
| 11 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(rank‘𝑥)
∈ V |
| 12 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑦 = (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ (rank‘𝑥) = (rank‘𝑥))) |
| 13 | 12 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑦 = (rank‘𝑥) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)))) |
| 14 | 11, 13 | spcev 3606 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 15 | 14 | eximi 1835 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 16 | | excom 2162 |
. . . . . . . . 9
⊢
(∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 17 | 15, 16 | sylibr 234 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 18 | | df-rex 3071 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥))) |
| 19 | | df-rex 3071 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 20 | 19 | exbii 1848 |
. . . . . . . 8
⊢
(∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
| 21 | 17, 18, 20 | 3imtr4i 292 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
| 22 | 10, 21 | syl 17 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
| 23 | | abn0 4385 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
| 24 | 22, 23 | sylibr 234 |
. . . . 5
⊢ (𝐴 ≠ ∅ → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) |
| 25 | 11 | dfiin2 5034 |
. . . . . 6
⊢ ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} |
| 26 | | rankon 9835 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
| 27 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑦 = (rank‘𝑥) → (𝑦 ∈ On ↔ (rank‘𝑥) ∈ On)) |
| 28 | 26, 27 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
| 29 | 28 | rexlimivw 3151 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
| 30 | 29 | abssi 4070 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On |
| 31 | | onint 7810 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
| 32 | 30, 31 | mpan 690 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
| 33 | 25, 32 | eqeltrid 2845 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
| 34 | | nfii1 5029 |
. . . . . . . . 9
⊢
Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
| 35 | 34 | nfeq2 2923 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
| 36 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ ∩
𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
| 37 | 35, 36 | rexbid 3274 |
. . . . . . 7
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
| 38 | 37 | elabg 3676 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
| 39 | 38 | ibi 267 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
| 40 | | ssid 4006 |
. . . . . . . . . 10
⊢
(rank‘𝑦)
⊆ (rank‘𝑦) |
| 41 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦)) |
| 42 | 41 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑦) ⊆ (rank‘𝑦))) |
| 43 | 42 | rspcev 3622 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (rank‘𝑦) ⊆ (rank‘𝑦)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 44 | 40, 43 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 45 | | iinss 5056 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 47 | | sseq1 4009 |
. . . . . . . 8
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑥) ⊆ (rank‘𝑦))) |
| 48 | 46, 47 | imbitrid 244 |
. . . . . . 7
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (𝑦 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) |
| 49 | 48 | ralrimiv 3145 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 50 | 49 | reximi 3084 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 51 | 24, 33, 39, 50 | 4syl 19 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 52 | | rabn0 4389 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
| 53 | 51, 52 | sylibr 234 |
. . 3
⊢ (𝐴 ≠ ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) |
| 54 | 53 | necon4i 2976 |
. 2
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ → 𝐴 = ∅) |
| 55 | 3, 54 | impbii 209 |
1
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |