Step | Hyp | Ref
| Expression |
1 | | difeq2 3722 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑋 ∖ 𝑥) = (𝑋 ∖ 𝑦)) |
2 | 1 | breq1d 4663 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑋 ∖ 𝑥) ≺ 𝑋 ↔ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
3 | 2 | elrab 3363 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
4 | | selpw 4165 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
5 | 4 | anbi1i 731 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋) ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
6 | 3, 5 | bitri 264 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋))) |
8 | | elex 3212 |
. . 3
⊢ (𝑋 ∈ dom card → 𝑋 ∈ V) |
9 | 8 | adantr 481 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ∈ V) |
10 | | difid 3948 |
. . . 4
⊢ (𝑋 ∖ 𝑋) = ∅ |
11 | | infn0 8222 |
. . . . . 6
⊢ (ω
≼ 𝑋 → 𝑋 ≠ ∅) |
12 | 11 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ≠ ∅) |
13 | | 0sdomg 8089 |
. . . . . 6
⊢ (𝑋 ∈ dom card → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
15 | 12, 14 | mpbird 247 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ∅
≺ 𝑋) |
16 | 10, 15 | syl5eqbr 4688 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑋 ∖ 𝑋) ≺ 𝑋) |
17 | | difeq2 3722 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋)) |
18 | 17 | breq1d 4663 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
19 | 18 | sbcieg 3468 |
. . . 4
⊢ (𝑋 ∈ dom card →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
20 | 19 | adantr 481 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
21 | 16, 20 | mpbird 247 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
[𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
22 | | sdomirr 8097 |
. . 3
⊢ ¬
𝑋 ≺ 𝑋 |
23 | | 0ex 4790 |
. . . . 5
⊢ ∅
∈ V |
24 | | difeq2 3722 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅)) |
25 | | dif0 3950 |
. . . . . . 7
⊢ (𝑋 ∖ ∅) = 𝑋 |
26 | 24, 25 | syl6eq 2672 |
. . . . . 6
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = 𝑋) |
27 | 26 | breq1d 4663 |
. . . . 5
⊢ (𝑦 = ∅ → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
28 | 23, 27 | sbcie 3470 |
. . . 4
⊢
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋) |
29 | 28 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
30 | 22, 29 | mtbiri 317 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ¬
[∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
31 | | simp1l 1085 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → 𝑋 ∈ dom card) |
32 | | difexg 4808 |
. . . . . 6
⊢ (𝑋 ∈ dom card → (𝑋 ∖ 𝑤) ∈ V) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑤) ∈ V) |
34 | | sscon 3744 |
. . . . . 6
⊢ (𝑤 ⊆ 𝑧 → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
35 | 34 | 3ad2ant3 1084 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
36 | | ssdomg 8001 |
. . . . 5
⊢ ((𝑋 ∖ 𝑤) ∈ V → ((𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤))) |
37 | 33, 35, 36 | sylc 65 |
. . . 4
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤)) |
38 | | domsdomtr 8095 |
. . . . 5
⊢ (((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ 𝑧) ≺ 𝑋) |
39 | 38 | ex 450 |
. . . 4
⊢ ((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
40 | 37, 39 | syl 17 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
41 | | vex 3203 |
. . . 4
⊢ 𝑤 ∈ V |
42 | | difeq2 3722 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑤)) |
43 | 42 | breq1d 4663 |
. . . 4
⊢ (𝑦 = 𝑤 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
44 | 41, 43 | sbcie 3470 |
. . 3
⊢
([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋) |
45 | | vex 3203 |
. . . 4
⊢ 𝑧 ∈ V |
46 | | difeq2 3722 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧)) |
47 | 46 | breq1d 4663 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋)) |
48 | 45, 47 | sbcie 3470 |
. . 3
⊢
([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋) |
49 | 40, 44, 48 | 3imtr4g 285 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 → [𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
50 | | infunsdom 9036 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
51 | 50 | ex 450 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋)) |
52 | | difindi 3881 |
. . . . . 6
⊢ (𝑋 ∖ (𝑧 ∩ 𝑤)) = ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) |
53 | 52 | breq1i 4660 |
. . . . 5
⊢ ((𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋 ↔ ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
54 | 51, 53 | syl6ibr 242 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
55 | 54 | 3ad2ant1 1082 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
56 | 48, 44 | anbi12i 733 |
. . 3
⊢
(([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) ↔ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
57 | 45 | inex1 4799 |
. . . 4
⊢ (𝑧 ∩ 𝑤) ∈ V |
58 | | difeq2 3722 |
. . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑧 ∩ 𝑤))) |
59 | 58 | breq1d 4663 |
. . . 4
⊢ (𝑦 = (𝑧 ∩ 𝑤) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
60 | 57, 59 | sbcie 3470 |
. . 3
⊢
([(𝑧 ∩
𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋) |
61 | 55, 56, 60 | 3imtr4g 285 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) → [(𝑧 ∩ 𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
62 | 7, 9, 21, 30, 49, 61 | isfild 21662 |
1
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ∈ (Fil‘𝑋)) |