Proof of Theorem scott0
Step | Hyp | Ref
| Expression |
1 | | rabeq 3394 |
. . 3
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}) |
2 | | rab0 4297 |
. . 3
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ |
3 | 1, 2 | eqtrdi 2794 |
. 2
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |
4 | | n0 4261 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
5 | | nfre1 3225 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) |
6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(rank‘𝑥) =
(rank‘𝑥) |
7 | | rspe 3223 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
8 | 6, 7 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
9 | 5, 8 | exlimi 2215 |
. . . . . . . 8
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
10 | 4, 9 | sylbi 220 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
11 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(rank‘𝑥)
∈ V |
12 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑦 = (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ (rank‘𝑥) = (rank‘𝑥))) |
13 | 12 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝑦 = (rank‘𝑥) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)))) |
14 | 11, 13 | spcev 3521 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
15 | 14 | eximi 1842 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
16 | | excom 2166 |
. . . . . . . . 9
⊢
(∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
17 | 15, 16 | sylibr 237 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
18 | | df-rex 3067 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥))) |
19 | | df-rex 3067 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
20 | 19 | exbii 1855 |
. . . . . . . 8
⊢
(∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
21 | 17, 18, 20 | 3imtr4i 295 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
22 | 10, 21 | syl 17 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
23 | | abn0 4295 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
24 | 22, 23 | sylibr 237 |
. . . . 5
⊢ (𝐴 ≠ ∅ → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) |
25 | 11 | dfiin2 4943 |
. . . . . 6
⊢ ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} |
26 | | rankon 9411 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
27 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑦 = (rank‘𝑥) → (𝑦 ∈ On ↔ (rank‘𝑥) ∈ On)) |
28 | 26, 27 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
29 | 28 | rexlimivw 3201 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
30 | 29 | abssi 3983 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On |
31 | | onint 7574 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
32 | 30, 31 | mpan 690 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
33 | 25, 32 | eqeltrid 2842 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
34 | | nfii1 4939 |
. . . . . . . . 9
⊢
Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
35 | 34 | nfeq2 2921 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
36 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ ∩
𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
37 | 35, 36 | rexbid 3239 |
. . . . . . 7
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
38 | 37 | elabg 3585 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
39 | 38 | ibi 270 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
40 | | ssid 3923 |
. . . . . . . . . 10
⊢
(rank‘𝑦)
⊆ (rank‘𝑦) |
41 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦)) |
42 | 41 | sseq1d 3932 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑦) ⊆ (rank‘𝑦))) |
43 | 42 | rspcev 3537 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (rank‘𝑦) ⊆ (rank‘𝑦)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
44 | 40, 43 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
45 | | iinss 4965 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
47 | | sseq1 3926 |
. . . . . . . 8
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑥) ⊆ (rank‘𝑦))) |
48 | 46, 47 | syl5ib 247 |
. . . . . . 7
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (𝑦 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) |
49 | 48 | ralrimiv 3104 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
50 | 49 | reximi 3166 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
51 | 24, 33, 39, 50 | 4syl 19 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
52 | | rabn0 4300 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
53 | 51, 52 | sylibr 237 |
. . 3
⊢ (𝐴 ≠ ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) |
54 | 53 | necon4i 2976 |
. 2
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ → 𝐴 = ∅) |
55 | 3, 54 | impbii 212 |
1
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |