| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ordon 7798 | . . . 4
⊢ Ord
On | 
| 2 |  | tz7.5 6404 | . . . 4
⊢ ((Ord On
∧ 𝐴 ⊆ On ∧
𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅) | 
| 3 | 1, 2 | mp3an1 1449 | . . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) →
∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅) | 
| 4 |  | ssel 3976 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On)) | 
| 5 | 4 | imdistani 568 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ On ∧ 𝑥 ∈ On)) | 
| 6 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆ On → (𝑧 ∈ 𝐴 → 𝑧 ∈ On)) | 
| 7 |  | ontri1 6417 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (𝑥 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑥)) | 
| 8 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ⊆ 𝑧 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧)) | 
| 9 | 7, 8 | biimtrrdi 254 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧))) | 
| 10 | 9 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (𝑧 ∈ On → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧)))) | 
| 11 | 6, 10 | sylan9 507 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧 ∈ 𝐴 → (¬ 𝑧 ∈ 𝑥 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧)))) | 
| 12 | 11 | com4r 94 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑥 → ((𝐴 ⊆ On ∧ 𝑥 ∈ On) → (𝑧 ∈ 𝐴 → (¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧)))) | 
| 13 | 12 | imp31 417 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) ∧ 𝑧 ∈ 𝐴) → (¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧)) | 
| 14 | 13 | ralimdva 3166 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → (∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 → ∀𝑧 ∈ 𝐴 𝑦 ∈ 𝑧)) | 
| 15 |  | disj 4449 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∩ 𝑥) = ∅ ↔ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥) | 
| 16 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V | 
| 17 | 16 | elint2 4952 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ∩ 𝐴
↔ ∀𝑧 ∈
𝐴 𝑦 ∈ 𝑧) | 
| 18 | 14, 15, 17 | 3imtr4g 296 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ On)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴)) | 
| 19 | 5, 18 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴)) → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴)) | 
| 20 | 19 | exp32 420 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 → (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → 𝑦 ∈ ∩ 𝐴)))) | 
| 21 | 20 | com4l 92 | . . . . . . . . . . . 12
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴)))) | 
| 22 | 21 | imp32 418 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴)) | 
| 23 | 22 | ssrdv 3988 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 ⊆ ∩ 𝐴) | 
| 24 |  | intss1 4962 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥) | 
| 25 | 24 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → ∩ 𝐴
⊆ 𝑥) | 
| 26 | 23, 25 | eqssd 4000 | . . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → 𝑥 = ∩ 𝐴) | 
| 27 | 26 | eleq1d 2825 | . . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑥 ∈ 𝐴 ↔ ∩ 𝐴 ∈ 𝐴)) | 
| 28 | 27 | biimpd 229 | . . . . . . 7
⊢ ((𝐴 ⊆ On ∧ (𝑥 ∈ 𝐴 ∧ (𝐴 ∩ 𝑥) = ∅)) → (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴)) | 
| 29 | 28 | exp32 420 | . . . . . 6
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → (𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴)))) | 
| 30 | 29 | com34 91 | . . . . 5
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴
∈ 𝐴)))) | 
| 31 | 30 | pm2.43d 53 | . . . 4
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → ((𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴
∈ 𝐴))) | 
| 32 | 31 | rexlimdv 3152 | . . 3
⊢ (𝐴 ⊆ On → (∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅ → ∩ 𝐴
∈ 𝐴)) | 
| 33 | 3, 32 | syl5 34 | . 2
⊢ (𝐴 ⊆ On → ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ 𝐴)) | 
| 34 | 33 | anabsi5 669 | 1
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ 𝐴) |