Proof of Theorem scott0
Step | Hyp | Ref
| Expression |
1 | | rabeq 3192 |
. . 3
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = {𝑥 ∈ ∅ ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)}) |
2 | | rab0 3955 |
. . 3
⊢ {𝑥 ∈ ∅ ∣
∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ |
3 | 1, 2 | syl6eq 2672 |
. 2
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |
4 | | n0 3931 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
5 | | nfre1 3005 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) |
6 | | eqid 2622 |
. . . . . . . . . 10
⊢
(rank‘𝑥) =
(rank‘𝑥) |
7 | | rspe 3003 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
8 | 6, 7 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
9 | 5, 8 | exlimi 2086 |
. . . . . . . 8
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
10 | 4, 9 | sylbi 207 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
11 | | fvex 6201 |
. . . . . . . . . . 11
⊢
(rank‘𝑥)
∈ V |
12 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑦 = (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ (rank‘𝑥) = (rank‘𝑥))) |
13 | 12 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝑦 = (rank‘𝑥) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)))) |
14 | 11, 13 | spcev 3300 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
15 | 14 | eximi 1762 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
16 | | excom 2042 |
. . . . . . . . 9
⊢
(∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
17 | 15, 16 | sylibr 224 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥)) → ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
18 | | df-rex 2918 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (rank‘𝑥) = (rank‘𝑥))) |
19 | | df-rex 2918 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
20 | 19 | exbii 1774 |
. . . . . . . 8
⊢
(∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = (rank‘𝑥))) |
21 | 17, 18, 20 | 3imtr4i 281 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
22 | 10, 21 | syl 17 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
23 | | abn0 3954 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)) |
24 | 22, 23 | sylibr 224 |
. . . . 5
⊢ (𝐴 ≠ ∅ → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) |
25 | 11 | dfiin2 4555 |
. . . . . 6
⊢ ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} |
26 | | rankon 8658 |
. . . . . . . . . 10
⊢
(rank‘𝑥)
∈ On |
27 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑦 = (rank‘𝑥) → (𝑦 ∈ On ↔ (rank‘𝑥) ∈ On)) |
28 | 26, 27 | mpbiri 248 |
. . . . . . . . 9
⊢ (𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
29 | 28 | rexlimivw 3029 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥) → 𝑦 ∈ On) |
30 | 29 | abssi 3677 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On |
31 | | onint 6995 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
32 | 30, 31 | mpan 706 |
. . . . . 6
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = (rank‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
33 | 25, 32 | syl5eqel 2705 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)}) |
34 | | nfii1 4551 |
. . . . . . . . 9
⊢
Ⅎ𝑥∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
35 | 34 | nfeq2 2780 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) |
36 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (𝑦 = (rank‘𝑥) ↔ ∩
𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
37 | 35, 36 | rexbid 3051 |
. . . . . . 7
⊢ (𝑦 = ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) → (∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥) ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
38 | 37 | elabg 3351 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥))) |
39 | 38 | ibi 256 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (rank‘𝑥)} → ∃𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥)) |
40 | | ssid 3624 |
. . . . . . . . . 10
⊢
(rank‘𝑦)
⊆ (rank‘𝑦) |
41 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (rank‘𝑥) = (rank‘𝑦)) |
42 | 41 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑦) ⊆ (rank‘𝑦))) |
43 | 42 | rspcev 3309 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (rank‘𝑦) ⊆ (rank‘𝑦)) → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
44 | 40, 43 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
45 | | iinss 4571 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
47 | | sseq1 3626 |
. . . . . . . 8
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (∩
𝑥 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑥) ⊆ (rank‘𝑦))) |
48 | 46, 47 | syl5ib 234 |
. . . . . . 7
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → (𝑦 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) |
49 | 48 | ralrimiv 2965 |
. . . . . 6
⊢ (∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
50 | 49 | reximi 3011 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∩ 𝑥 ∈ 𝐴 (rank‘𝑥) = (rank‘𝑥) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
51 | 24, 33, 39, 50 | 4syl 19 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
52 | | rabn0 3958 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)) |
53 | 51, 52 | sylibr 224 |
. . 3
⊢ (𝐴 ≠ ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ≠ ∅) |
54 | 53 | necon4i 2829 |
. 2
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅ → 𝐴 = ∅) |
55 | 3, 54 | impbii 199 |
1
⊢ (𝐴 = ∅ ↔ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} = ∅) |