Proof of Theorem scott0
Step | Hyp | Ref
| Expression |
1 | | rabeq 3485 |
. . 3
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}) |
2 | | rab0 4339 |
. . 3
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ |
3 | 1, 2 | syl6eq 2874 |
. 2
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |
4 | | n0 4312 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
5 | | nfre1 3308 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) |
6 | | eqid 2823 |
. . . . . . . . . 10
⊢
(rank‘𝑥) =
(rank‘𝑥) |
7 | | rspe 3306 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
8 | 6, 7 | mpan2 689 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
9 | 5, 8 | exlimi 2217 |
. . . . . . . 8
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
10 | 4, 9 | sylbi 219 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
11 | | fvex 6685 |
. . . . . . . . . . 11
⊢
(rank‘𝑥)
∈ V |
12 | | eqeq1 2827 |
. . . . . . . . . . . 12
⊢ (𝑦 = (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ (rank‘𝑥) = (rank‘𝑥))) |
13 | 12 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑦 = (rank‘𝑥) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)))) |
14 | 11, 13 | spcev 3609 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
15 | 14 | eximi 1835 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
16 | | excom 2169 |
. . . . . . . . 9
⊢
(∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
17 | 15, 16 | sylibr 236 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
18 | | df-rex 3146 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥))) |
19 | | df-rex 3146 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
20 | 19 | exbii 1848 |
. . . . . . . 8
⊢
(∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
21 | 17, 18, 20 | 3imtr4i 294 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
22 | 10, 21 | syl 17 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
23 | | abn0 4338 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
24 | 22, 23 | sylibr 236 |
. . . . 5
⊢ (𝐴 ≠ ∅ → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) |
25 | 11 | dfiin2 4961 |
. . . . . 6
⊢ ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} |
26 | | rankon 9226 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
27 | | eleq1 2902 |
. . . . . . . . . 10
⊢ (𝑦 = (rank‘𝑥) → (𝑦 ∈ On ↔ (rank‘𝑥) ∈ On)) |
28 | 26, 27 | mpbiri 260 |
. . . . . . . . 9
⊢ (𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
29 | 28 | rexlimivw 3284 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
30 | 29 | abssi 4048 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On |
31 | | onint 7512 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
32 | 30, 31 | mpan 688 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
33 | 25, 32 | eqeltrid 2919 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
34 | | nfii1 4956 |
. . . . . . . . 9
⊢
Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
35 | 34 | nfeq2 2997 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
36 | | eqeq1 2827 |
. . . . . . . 8
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ ∩
𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
37 | 35, 36 | rexbid 3322 |
. . . . . . 7
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
38 | 37 | elabg 3668 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
39 | 38 | ibi 269 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
40 | | ssid 3991 |
. . . . . . . . . 10
⊢
(rank‘𝑦)
⊆ (rank‘𝑦) |
41 | | fveq2 6672 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦)) |
42 | 41 | sseq1d 4000 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑦) ⊆ (rank‘𝑦))) |
43 | 42 | rspcev 3625 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (rank‘𝑦) ⊆ (rank‘𝑦)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
44 | 40, 43 | mpan2 689 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
45 | | iinss 4982 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
47 | | sseq1 3994 |
. . . . . . . 8
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑥) ⊆ (rank‘𝑦))) |
48 | 46, 47 | syl5ib 246 |
. . . . . . 7
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (𝑦 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) |
49 | 48 | ralrimiv 3183 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
50 | 49 | reximi 3245 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
51 | 24, 33, 39, 50 | 4syl 19 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
52 | | rabn0 4341 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
53 | 51, 52 | sylibr 236 |
. . 3
⊢ (𝐴 ≠ ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) |
54 | 53 | necon4i 3053 |
. 2
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ → 𝐴 = ∅) |
55 | 3, 54 | impbii 211 |
1
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |