| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfepfr 5669 | . 2
⊢ ( E Fr On
↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) | 
| 2 |  | n0 4353 | . . . 4
⊢ (𝑥 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) | 
| 3 |  | ineq2 4214 | . . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦)) | 
| 4 | 3 | eqeq1d 2739 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅)) | 
| 5 | 4 | rspcev 3622 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) | 
| 6 | 5 | adantll 714 | . . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) | 
| 7 |  | inss1 4237 | . . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 | 
| 8 |  | ssel2 3978 | . . . . . . . . . . 11
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) | 
| 9 |  | eloni 6394 | . . . . . . . . . . 11
⊢ (𝑦 ∈ On → Ord 𝑦) | 
| 10 |  | ordfr 6399 | . . . . . . . . . . 11
⊢ (Ord
𝑦 → E Fr 𝑦) | 
| 11 | 8, 9, 10 | 3syl 18 | . . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦) | 
| 12 |  | inss2 4238 | . . . . . . . . . . 11
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦 | 
| 13 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 14 | 13 | inex1 5317 | . . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝑦) ∈ V | 
| 15 | 14 | epfrc 5670 | . . . . . . . . . . 11
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) | 
| 16 | 12, 15 | mp3an2 1451 | . . . . . . . . . 10
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) | 
| 17 | 11, 16 | sylan 580 | . . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) | 
| 18 |  | inass 4228 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧)) | 
| 19 | 8, 9 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) | 
| 20 |  | elinel2 4202 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦) | 
| 21 |  | ordelss 6400 | . . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦) | 
| 22 | 19, 20, 21 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦) | 
| 23 |  | sseqin2 4223 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧) | 
| 24 | 22, 23 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧) | 
| 25 | 24 | ineq2d 4220 | . . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧)) | 
| 26 | 18, 25 | eqtrid 2789 | . . . . . . . . . . . 12
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧)) | 
| 27 | 26 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅)) | 
| 28 | 27 | rexbidva 3177 | . . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) | 
| 29 | 28 | adantr 480 | . . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) | 
| 30 | 17, 29 | mpbid 232 | . . . . . . . 8
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅) | 
| 31 |  | ssrexv 4053 | . . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) | 
| 32 | 7, 30, 31 | mpsyl 68 | . . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) | 
| 33 | 6, 32 | pm2.61dane 3029 | . . . . . 6
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) | 
| 34 | 33 | ex 412 | . . . . 5
⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) | 
| 35 | 34 | exlimdv 1933 | . . . 4
⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) | 
| 36 | 2, 35 | biimtrid 242 | . . 3
⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) | 
| 37 | 36 | imp 406 | . 2
⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) | 
| 38 | 1, 37 | mpgbir 1799 | 1
⊢  E Fr
On |