Step | Hyp | Ref
| Expression |
1 | | dfepfr 5099 |
. 2
⊢ ( E Fr On
↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
2 | | n0 3931 |
. . . 4
⊢ (𝑥 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
3 | | ineq2 3808 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦)) |
4 | 3 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅)) |
5 | 4 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
6 | 5 | adantll 750 |
. . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
7 | | inss1 3833 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
8 | | ssel2 3598 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
9 | | eloni 5733 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → Ord 𝑦) |
10 | | ordfr 5738 |
. . . . . . . . . . 11
⊢ (Ord
𝑦 → E Fr 𝑦) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦) |
12 | | inss2 3834 |
. . . . . . . . . . 11
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦 |
13 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
14 | 13 | inex1 4799 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝑦) ∈ V |
15 | 14 | epfrc 5100 |
. . . . . . . . . . 11
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
16 | 12, 15 | mp3an2 1412 |
. . . . . . . . . 10
⊢ (( E Fr
𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
17 | 11, 16 | sylan 488 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅) |
18 | | inass 3823 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧)) |
19 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
20 | | elinel2 3800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦) |
21 | | ordelss 5739 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦) |
22 | 19, 20, 21 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦) |
23 | | sseqin2 3817 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧) |
24 | 22, 23 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧) |
25 | 24 | ineq2d 3814 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧)) |
26 | 18, 25 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧)) |
27 | 26 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅)) |
28 | 27 | rexbidva 3049 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)) |
30 | 17, 29 | mpbid 222 |
. . . . . . . 8
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅) |
31 | | ssrexv 3667 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
32 | 7, 30, 31 | mpsyl 68 |
. . . . . . 7
⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
33 | 6, 32 | pm2.61dane 2881 |
. . . . . 6
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
34 | 33 | ex 450 |
. . . . 5
⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
35 | 34 | exlimdv 1861 |
. . . 4
⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
36 | 2, 35 | syl5bi 232 |
. . 3
⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)) |
37 | 36 | imp 445 |
. 2
⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) →
∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅) |
38 | 1, 37 | mpgbir 1726 |
1
⊢ E Fr
On |