Proof of Theorem tfi
Step | Hyp | Ref
| Expression |
1 | | eldifn 3733 |
. . . . . . . . 9
⊢ (𝑥 ∈ (On ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
2 | 1 | adantl 482 |
. . . . . . . 8
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
3 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (On ∖ 𝐴) → 𝑥 ∈ On) |
4 | | onss 6990 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
5 | | difin0ss 3946 |
. . . . . . . . . . . . 13
⊢ (((On
∖ 𝐴) ∩ 𝑥) = ∅ → (𝑥 ⊆ On → 𝑥 ⊆ 𝐴)) |
6 | 4, 5 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (((On ∖
𝐴) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐴)) |
7 | 6 | imim1d 82 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → ((𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴))) |
8 | 7 | a2i 14 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝑥 ∈ On → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴))) |
9 | 3, 8 | syl5 34 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝑥 ∈ (On ∖ 𝐴) → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴))) |
10 | 9 | imp 445 |
. . . . . . . 8
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴)) |
11 | 2, 10 | mtod 189 |
. . . . . . 7
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅) |
12 | 11 | ex 450 |
. . . . . 6
⊢ ((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝑥 ∈ (On ∖ 𝐴) → ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅)) |
13 | 12 | ralimi2 2949 |
. . . . 5
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → ∀𝑥 ∈ (On ∖ 𝐴) ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅) |
14 | | ralnex 2992 |
. . . . 5
⊢
(∀𝑥 ∈
(On ∖ 𝐴) ¬ ((On
∖ 𝐴) ∩ 𝑥) = ∅ ↔ ¬
∃𝑥 ∈ (On ∖
𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) |
15 | 13, 14 | sylib 208 |
. . . 4
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → ¬ ∃𝑥 ∈ (On ∖ 𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) |
16 | | ssdif0 3942 |
. . . . . 6
⊢ (On
⊆ 𝐴 ↔ (On
∖ 𝐴) =
∅) |
17 | 16 | necon3bbii 2841 |
. . . . 5
⊢ (¬ On
⊆ 𝐴 ↔ (On
∖ 𝐴) ≠
∅) |
18 | | ordon 6982 |
. . . . . 6
⊢ Ord
On |
19 | | difss 3737 |
. . . . . 6
⊢ (On
∖ 𝐴) ⊆
On |
20 | | tz7.5 5744 |
. . . . . 6
⊢ ((Ord On
∧ (On ∖ 𝐴)
⊆ On ∧ (On ∖ 𝐴) ≠ ∅) → ∃𝑥 ∈ (On ∖ 𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) |
21 | 18, 19, 20 | mp3an12 1414 |
. . . . 5
⊢ ((On
∖ 𝐴) ≠ ∅
→ ∃𝑥 ∈ (On
∖ 𝐴)((On ∖
𝐴) ∩ 𝑥) = ∅) |
22 | 17, 21 | sylbi 207 |
. . . 4
⊢ (¬ On
⊆ 𝐴 →
∃𝑥 ∈ (On ∖
𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) |
23 | 15, 22 | nsyl2 142 |
. . 3
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → On ⊆ 𝐴) |
24 | 23 | anim2i 593 |
. 2
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝐴 ⊆ On ∧ On ⊆ 𝐴)) |
25 | | eqss 3618 |
. 2
⊢ (𝐴 = On ↔ (𝐴 ⊆ On ∧ On ⊆ 𝐴)) |
26 | 24, 25 | sylibr 224 |
1
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On) |