| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | idn1 44599 | . . . . . 6
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ) | 
| 2 |  | simpr 484 | . . . . . 6
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅) | 
| 3 | 1, 2 | e1a 44652 | . . . . 5
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ≠ ∅   ) | 
| 4 |  | exmid 894 | . . . . . . . . . 10
⊢ ((𝑎 ∩ 𝑥) = ∅ ∨ ¬ (𝑎 ∩ 𝑥) = ∅) | 
| 5 |  | onfrALTlem1VD 44915 | . . . . . . . . . . 11
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   ) | 
| 6 | 5 | in2an 44633 | . . . . . . . . . 10
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   ((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 7 |  | onfrALTlem2VD 44914 | . . . . . . . . . . 11
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   ) | 
| 8 | 7 | in2an 44633 | . . . . . . . . . 10
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   (¬
(𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 9 |  | pm2.61 192 | . . . . . . . . . . 11
⊢ (((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | 
| 10 | 9 | a1i 11 | . . . . . . . . . 10
⊢ (((𝑎 ∩ 𝑥) = ∅ ∨ ¬ (𝑎 ∩ 𝑥) = ∅) → (((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))) | 
| 11 | 4, 6, 8, 10 | e022 44666 | . . . . . . . . 9
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   ) | 
| 12 | 11 | in2 44630 | . . . . . . . 8
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 13 | 12 | gen11 44641 | . . . . . . 7
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 14 |  | 19.23v 1941 | . . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) ↔ (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | 
| 15 | 14 | biimpi 216 | . . . . . . 7
⊢
(∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | 
| 16 | 13, 15 | e1a 44652 | . . . . . 6
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 17 |  | n0 4352 | . . . . . 6
⊢ (𝑎 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑎) | 
| 18 |  | imbi1 347 | . . . . . . 7
⊢ ((𝑎 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑎) → ((𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) ↔ (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))) | 
| 19 | 18 | biimprcd 250 | . . . . . 6
⊢
((∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((𝑎 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑎) → (𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))) | 
| 20 | 16, 17, 19 | e10 44719 | . . . . 5
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ≠ ∅ →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   ) | 
| 21 |  | pm2.27 42 | . . . . 5
⊢ (𝑎 ≠ ∅ → ((𝑎 ≠ ∅ →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | 
| 22 | 3, 20, 21 | e11 44713 | . . . 4
⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   ) | 
| 23 | 22 | in1 44596 | . . 3
⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) | 
| 24 | 23 | ax-gen 1794 | . 2
⊢
∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) | 
| 25 |  | dfepfr 5668 | . . 3
⊢ ( E Fr On
↔ ∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)) | 
| 26 | 25 | biimpri 228 | . 2
⊢
(∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) →
∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → E Fr On) | 
| 27 | 24, 26 | e0a 44797 | 1
⊢  E Fr
On |