| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 2 |  | inss2 4237 | . . . . 5
⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥 | 
| 3 | 1, 2 | ssexi 5321 | . . . 4
⊢ (𝑎 ∩ 𝑥) ∈ V | 
| 4 |  | idn2 44638 | . . . . . . . . . . 11
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ) | 
| 5 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ 𝑎) | 
| 6 | 4, 5 | e2 44656 | . . . . . . . . . 10
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   ) | 
| 7 |  | idn1 44599 | . . . . . . . . . . 11
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ) | 
| 8 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ On) | 
| 9 | 7, 8 | e1a 44652 | . . . . . . . . . 10
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   ) | 
| 10 |  | ssel 3976 | . . . . . . . . . . 11
⊢ (𝑎 ⊆ On → (𝑥 ∈ 𝑎 → 𝑥 ∈ On)) | 
| 11 | 10 | com12 32 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑎 → (𝑎 ⊆ On → 𝑥 ∈ On)) | 
| 12 | 6, 9, 11 | e21 44755 | . . . . . . . . 9
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   ) | 
| 13 |  | eloni 6393 | . . . . . . . . 9
⊢ (𝑥 ∈ On → Ord 𝑥) | 
| 14 | 12, 13 | e2 44656 | . . . . . . . 8
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   ) | 
| 15 |  | ordwe 6396 | . . . . . . . 8
⊢ (Ord
𝑥 → E We 𝑥) | 
| 16 | 14, 15 | e2 44656 | . . . . . . 7
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E We
𝑥   ) | 
| 17 |  | wess 5670 | . . . . . . . 8
⊢ ((𝑎 ∩ 𝑥) ⊆ 𝑥 → ( E We 𝑥 → E We (𝑎 ∩ 𝑥))) | 
| 18 | 17 | com12 32 | . . . . . . 7
⊢ ( E We
𝑥 → ((𝑎 ∩ 𝑥) ⊆ 𝑥 → E We (𝑎 ∩ 𝑥))) | 
| 19 | 16, 2, 18 | e20 44752 | . . . . . 6
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E We
(𝑎 ∩ 𝑥)   ) | 
| 20 |  | wefr 5674 | . . . . . 6
⊢ ( E We
(𝑎 ∩ 𝑥) → E Fr (𝑎 ∩ 𝑥)) | 
| 21 | 19, 20 | e2 44656 | . . . . 5
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    E Fr
(𝑎 ∩ 𝑥)   ) | 
| 22 |  | dfepfr 5668 | . . . . . 6
⊢ ( E Fr
(𝑎 ∩ 𝑥) ↔ ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)) | 
| 23 | 22 | biimpi 216 | . . . . 5
⊢ ( E Fr
(𝑎 ∩ 𝑥) → ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)) | 
| 24 | 21, 23 | e2 44656 | . . . 4
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)   ) | 
| 25 |  | spsbc 3800 | . . . 4
⊢ ((𝑎 ∩ 𝑥) ∈ V → (∀𝑏((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) → [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))) | 
| 26 | 3, 24, 25 | e02 44722 | . . 3
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   [(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)   ) | 
| 27 |  | onfrALTlem5 44567 | . . 3
⊢
([(𝑎 ∩
𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) | 
| 28 | 26, 27 | e2bi 44657 | . 2
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ) | 
| 29 |  | ssid 4005 | . . 3
⊢ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) | 
| 30 |  | simpr 484 | . . . . 5
⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ¬ (𝑎 ∩ 𝑥) = ∅) | 
| 31 | 4, 30 | e2 44656 | . . . 4
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶    ¬
(𝑎 ∩ 𝑥) = ∅   ) | 
| 32 |  | df-ne 2940 | . . . . 5
⊢ ((𝑎 ∩ 𝑥) ≠ ∅ ↔ ¬ (𝑎 ∩ 𝑥) = ∅) | 
| 33 | 32 | biimpri 228 | . . . 4
⊢ (¬
(𝑎 ∩ 𝑥) = ∅ → (𝑎 ∩ 𝑥) ≠ ∅) | 
| 34 | 31, 33 | e2 44656 | . . 3
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑎 ∩ 𝑥) ≠ ∅   ) | 
| 35 |  | pm3.2 469 | . . 3
⊢ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) → ((𝑎 ∩ 𝑥) ≠ ∅ → ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))) | 
| 36 | 29, 34, 35 | e02 44722 | . 2
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅)   ) | 
| 37 |  | id 22 | . 2
⊢ ((((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)) | 
| 38 | 28, 36, 37 | e22 44696 | 1
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   ) |