Proof of Theorem tfi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldifn 4131 | . . . . . . . . 9
⊢ (𝑥 ∈ (On ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) | 
| 2 | 1 | adantl 481 | . . . . . . . 8
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) | 
| 3 |  | onss 7806 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) | 
| 4 |  | difin0ss 4372 | . . . . . . . . . . . 12
⊢ (((On
∖ 𝐴) ∩ 𝑥) = ∅ → (𝑥 ⊆ On → 𝑥 ⊆ 𝐴)) | 
| 5 | 3, 4 | syl5com 31 | . . . . . . . . . . 11
⊢ (𝑥 ∈ On → (((On ∖
𝐴) ∩ 𝑥) = ∅ → 𝑥 ⊆ 𝐴)) | 
| 6 | 5 | imim1d 82 | . . . . . . . . . 10
⊢ (𝑥 ∈ On → ((𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴))) | 
| 7 | 6 | a2i 14 | . . . . . . . . 9
⊢ ((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝑥 ∈ On → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴))) | 
| 8 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝑥 ∈ (On ∖ 𝐴) → 𝑥 ∈ On) | 
| 9 | 7, 8 | impel 505 | . . . . . . . 8
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → (((On ∖ 𝐴) ∩ 𝑥) = ∅ → 𝑥 ∈ 𝐴)) | 
| 10 | 2, 9 | mtod 198 | . . . . . . 7
⊢ (((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) ∧ 𝑥 ∈ (On ∖ 𝐴)) → ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 11 | 10 | ex 412 | . . . . . 6
⊢ ((𝑥 ∈ On → (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝑥 ∈ (On ∖ 𝐴) → ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅)) | 
| 12 | 11 | ralimi2 3077 | . . . . 5
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → ∀𝑥 ∈ (On ∖ 𝐴) ¬ ((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 13 |  | ralnex 3071 | . . . . 5
⊢
(∀𝑥 ∈
(On ∖ 𝐴) ¬ ((On
∖ 𝐴) ∩ 𝑥) = ∅ ↔ ¬
∃𝑥 ∈ (On ∖
𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 14 | 12, 13 | sylib 218 | . . . 4
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → ¬ ∃𝑥 ∈ (On ∖ 𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 15 |  | ssdif0 4365 | . . . . . 6
⊢ (On
⊆ 𝐴 ↔ (On
∖ 𝐴) =
∅) | 
| 16 | 15 | necon3bbii 2987 | . . . . 5
⊢ (¬ On
⊆ 𝐴 ↔ (On
∖ 𝐴) ≠
∅) | 
| 17 |  | ordon 7798 | . . . . . 6
⊢ Ord
On | 
| 18 |  | difss 4135 | . . . . . 6
⊢ (On
∖ 𝐴) ⊆
On | 
| 19 |  | tz7.5 6404 | . . . . . 6
⊢ ((Ord On
∧ (On ∖ 𝐴)
⊆ On ∧ (On ∖ 𝐴) ≠ ∅) → ∃𝑥 ∈ (On ∖ 𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 20 | 17, 18, 19 | mp3an12 1452 | . . . . 5
⊢ ((On
∖ 𝐴) ≠ ∅
→ ∃𝑥 ∈ (On
∖ 𝐴)((On ∖
𝐴) ∩ 𝑥) = ∅) | 
| 21 | 16, 20 | sylbi 217 | . . . 4
⊢ (¬ On
⊆ 𝐴 →
∃𝑥 ∈ (On ∖
𝐴)((On ∖ 𝐴) ∩ 𝑥) = ∅) | 
| 22 | 14, 21 | nsyl2 141 | . . 3
⊢
(∀𝑥 ∈ On
(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → On ⊆ 𝐴) | 
| 23 | 22 | anim2i 617 | . 2
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → (𝐴 ⊆ On ∧ On ⊆ 𝐴)) | 
| 24 |  | eqss 3998 | . 2
⊢ (𝐴 = On ↔ (𝐴 ⊆ On ∧ On ⊆ 𝐴)) | 
| 25 | 23, 24 | sylibr 234 | 1
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ On (𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) → 𝐴 = On) |