Step | Hyp | Ref
| Expression |
1 | | ssralv 3991 |
. . . . 5
⊢ (𝑧 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥))) |
2 | | dfon2lem8 33745 |
. . . . . . . 8
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧) ∧ ∩ 𝑧
∈ 𝑧)) |
3 | 2 | simprd 495 |
. . . . . . 7
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∩ 𝑧 ∈ 𝑧) |
4 | | intss1 4899 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑡) |
5 | 2 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) |
6 | | intex 5264 |
. . . . . . . . . . 11
⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧
∈ V) |
7 | | dfon2lem3 33740 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ 𝑧
∈ V → (∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧) → (Tr ∩ 𝑧
∧ ∀𝑥 ∈
∩ 𝑧 ¬ 𝑥 ∈ 𝑥))) |
8 | 7 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (Tr ∩ 𝑧
∧ ∀𝑥 ∈
∩ 𝑧 ¬ 𝑥 ∈ 𝑥)) |
9 | 8 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → ∀𝑥 ∈ ∩ 𝑧
¬ 𝑥 ∈ 𝑥) |
10 | | untelirr 33628 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
∩ 𝑧 ¬ 𝑥 ∈ 𝑥 → ¬ ∩
𝑧 ∈ ∩ 𝑧) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → ¬ ∩ 𝑧
∈ ∩ 𝑧) |
12 | | eleq1 2827 |
. . . . . . . . . . . . . . 15
⊢ (∩ 𝑧 =
𝑡 → (∩ 𝑧
∈ ∩ 𝑧 ↔ 𝑡 ∈ ∩ 𝑧)) |
13 | 12 | notbid 317 |
. . . . . . . . . . . . . 14
⊢ (∩ 𝑧 =
𝑡 → (¬ ∩ 𝑧
∈ ∩ 𝑧 ↔ ¬ 𝑡 ∈ ∩ 𝑧)) |
14 | 11, 13 | syl5ibcom 244 |
. . . . . . . . . . . . 13
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (∩ 𝑧 =
𝑡 → ¬ 𝑡 ∈ ∩ 𝑧)) |
15 | 14 | a1dd 50 |
. . . . . . . . . . . 12
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (∩ 𝑧 =
𝑡 → (∩ 𝑧
⊆ 𝑡 → ¬
𝑡 ∈ ∩ 𝑧))) |
16 | 8 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → Tr ∩ 𝑧) |
17 | | trss 5204 |
. . . . . . . . . . . . . . . . 17
⊢ (Tr ∩ 𝑧
→ (𝑡 ∈ ∩ 𝑧
→ 𝑡 ⊆ ∩ 𝑧)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (𝑡 ∈ ∩ 𝑧 → 𝑡 ⊆ ∩ 𝑧)) |
19 | | eqss 3940 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ 𝑧 =
𝑡 ↔ (∩ 𝑧
⊆ 𝑡 ∧ 𝑡 ⊆ ∩ 𝑧)) |
20 | 19 | simplbi2com 502 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ⊆ ∩ 𝑧
→ (∩ 𝑧 ⊆ 𝑡 → ∩ 𝑧 = 𝑡)) |
21 | 18, 20 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (𝑡 ∈ ∩ 𝑧 → (∩ 𝑧
⊆ 𝑡 → ∩ 𝑧 =
𝑡))) |
22 | 21 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (∩ 𝑧
⊆ 𝑡 → (𝑡 ∈ ∩ 𝑧
→ ∩ 𝑧 = 𝑡))) |
23 | | con3 153 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ∩ 𝑧
→ ∩ 𝑧 = 𝑡) → (¬ ∩
𝑧 = 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧)) |
24 | 22, 23 | syl6 35 |
. . . . . . . . . . . . 13
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (∩ 𝑧
⊆ 𝑡 → (¬
∩ 𝑧 = 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧))) |
25 | 24 | com23 86 |
. . . . . . . . . . . 12
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (¬ ∩ 𝑧 =
𝑡 → (∩ 𝑧
⊆ 𝑡 → ¬
𝑡 ∈ ∩ 𝑧))) |
26 | 15, 25 | pm2.61d 179 |
. . . . . . . . . . 11
⊢ ((∩ 𝑧
∈ V ∧ ∀𝑢((𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧)) → (∩ 𝑧
⊆ 𝑡 → ¬
𝑡 ∈ ∩ 𝑧)) |
27 | 6, 26 | sylanb 580 |
. . . . . . . . . 10
⊢ ((𝑧 ≠ ∅ ∧
∀𝑢((𝑢 ⊊ ∩ 𝑧
∧ Tr 𝑢) → 𝑢 ∈ ∩ 𝑧))
→ (∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧)) |
28 | 5, 27 | syldan 590 |
. . . . . . . . 9
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧)) |
29 | 4, 28 | syl5 34 |
. . . . . . . 8
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝑧 → ¬ 𝑡 ∈ ∩ 𝑧)) |
30 | 29 | ralrimiv 3108 |
. . . . . . 7
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧) |
31 | | eleq2 2828 |
. . . . . . . . . 10
⊢ (𝑤 = ∩
𝑧 → (𝑡 ∈ 𝑤 ↔ 𝑡 ∈ ∩ 𝑧)) |
32 | 31 | notbid 317 |
. . . . . . . . 9
⊢ (𝑤 = ∩
𝑧 → (¬ 𝑡 ∈ 𝑤 ↔ ¬ 𝑡 ∈ ∩ 𝑧)) |
33 | 32 | ralbidv 3122 |
. . . . . . . 8
⊢ (𝑤 = ∩
𝑧 → (∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ↔ ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧)) |
34 | 33 | rspcev 3560 |
. . . . . . 7
⊢ ((∩ 𝑧
∈ 𝑧 ∧
∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤) |
35 | 3, 30, 34 | syl2anc 583 |
. . . . . 6
⊢ ((𝑧 ≠ ∅ ∧
∀𝑥 ∈ 𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤) |
36 | 35 | expcom 413 |
. . . . 5
⊢
(∀𝑥 ∈
𝑧 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑧 ≠ ∅ → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
37 | 1, 36 | syl6com 37 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑧 ⊆ 𝐴 → (𝑧 ≠ ∅ → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤))) |
38 | 37 | impd 410 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
39 | 38 | alrimiv 1933 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
40 | | df-fr 5543 |
. . 3
⊢ ( E Fr
𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤)) |
41 | | epel 5497 |
. . . . . . . 8
⊢ (𝑡 E 𝑤 ↔ 𝑡 ∈ 𝑤) |
42 | 41 | notbii 319 |
. . . . . . 7
⊢ (¬
𝑡 E 𝑤 ↔ ¬ 𝑡 ∈ 𝑤) |
43 | 42 | ralbii 3092 |
. . . . . 6
⊢
(∀𝑡 ∈
𝑧 ¬ 𝑡 E 𝑤 ↔ ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤) |
44 | 43 | rexbii 3179 |
. . . . 5
⊢
(∃𝑤 ∈
𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ↔ ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤) |
45 | 44 | imbi2i 335 |
. . . 4
⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
46 | 45 | albii 1825 |
. . 3
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤) ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
47 | 40, 46 | bitri 274 |
. 2
⊢ ( E Fr
𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑤 ∈ 𝑧 ∀𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤)) |
48 | 39, 47 | sylibr 233 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴) |