| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssid 4005 | . . 3
⊢ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) | 
| 2 |  | simpr 484 | . . . . 5
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ¬ (𝑎 ∩ 𝑥) = ∅) | 
| 3 | 2 | a1i 11 | . . . 4
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ¬ (𝑎 ∩ 𝑥) = ∅)) | 
| 4 |  | df-ne 2940 | . . . 4
⊢ ((𝑎 ∩ 𝑥) ≠ ∅ ↔ ¬ (𝑎 ∩ 𝑥) = ∅) | 
| 5 | 3, 4 | imbitrrdi 252 | . . 3
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → (𝑎 ∩ 𝑥) ≠ ∅)) | 
| 6 |  | pm3.2 469 | . . 3
⊢ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) → ((𝑎 ∩ 𝑥) ≠ ∅ → ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))) | 
| 7 | 1, 5, 6 | mpsylsyld 69 | . 2
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))) | 
| 8 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 9 | 8 | inex2 5317 | . . . 4
⊢ (𝑎 ∩ 𝑥) ∈ V | 
| 10 |  | inss2 4237 | . . . . . . 7
⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥 | 
| 11 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ On) | 
| 12 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ 𝑎) | 
| 13 |  | ssel 3976 | . . . . . . . . . 10
⊢ (𝑎 ⊆ On → (𝑥 ∈ 𝑎 → 𝑥 ∈ On)) | 
| 14 | 11, 12, 13 | syl2im 40 | . . . . . . . . 9
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ On)) | 
| 15 |  | eloni 6393 | . . . . . . . . 9
⊢ (𝑥 ∈ On → Ord 𝑥) | 
| 16 | 14, 15 | syl6 35 | . . . . . . . 8
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → Ord 𝑥)) | 
| 17 |  | ordwe 6396 | . . . . . . . 8
⊢ (Ord
𝑥 → E We 𝑥) | 
| 18 | 16, 17 | syl6 35 | . . . . . . 7
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E We 𝑥)) | 
| 19 |  | wess 5670 | . . . . . . 7
⊢ ((𝑎 ∩ 𝑥) ⊆ 𝑥 → ( E We 𝑥 → E We (𝑎 ∩ 𝑥))) | 
| 20 | 10, 18, 19 | mpsylsyld 69 | . . . . . 6
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E We (𝑎 ∩ 𝑥))) | 
| 21 |  | wefr 5674 | . . . . . 6
⊢ ( E We
(𝑎 ∩ 𝑥) → E Fr (𝑎 ∩ 𝑥)) | 
| 22 | 20, 21 | syl6 35 | . . . . 5
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → E Fr (𝑎 ∩ 𝑥))) | 
| 23 |  | dfepfr 5668 | . . . . 5
⊢ ( E Fr
(𝑎 ∩ 𝑥) ↔ ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)) | 
| 24 | 22, 23 | imbitrdi 251 | . . . 4
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) | 
| 25 |  | spsbc 3800 | . . . 4
⊢ ((𝑎 ∩ 𝑥) ∈ V → (∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) → [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) | 
| 26 | 9, 24, 25 | mpsylsyld 69 | . . 3
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) | 
| 27 |  | onfrALTlem5 44567 | . . 3
⊢
([(𝑎 ∩
𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) | 
| 28 | 26, 27 | imbitrdi 251 | . 2
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))) | 
| 29 | 7, 28 | mpdd 43 | 1
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) |