Step | Hyp | Ref
| Expression |
1 | | difeq2 4044 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑋 ∖ 𝑥) = (𝑋 ∖ 𝑦)) |
2 | 1 | breq1d 5040 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑋 ∖ 𝑥) ≺ 𝑋 ↔ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
3 | 2 | elrab 3628 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
4 | | velpw 4502 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
5 | 4 | anbi1i 626 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋) ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
6 | 3, 5 | bitri 278 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋))) |
8 | | simpl 486 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ∈ dom
card) |
9 | | difid 4284 |
. . . 4
⊢ (𝑋 ∖ 𝑋) = ∅ |
10 | | infn0 8764 |
. . . . . 6
⊢ (ω
≼ 𝑋 → 𝑋 ≠ ∅) |
11 | 10 | adantl 485 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ≠ ∅) |
12 | | 0sdomg 8630 |
. . . . . 6
⊢ (𝑋 ∈ dom card → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
14 | 11, 13 | mpbird 260 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ∅
≺ 𝑋) |
15 | 9, 14 | eqbrtrid 5065 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑋 ∖ 𝑋) ≺ 𝑋) |
16 | | difeq2 4044 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋)) |
17 | 16 | breq1d 5040 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
18 | 17 | sbcieg 3758 |
. . . 4
⊢ (𝑋 ∈ dom card →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
19 | 18 | adantr 484 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
20 | 15, 19 | mpbird 260 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
[𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
21 | | sdomirr 8638 |
. . 3
⊢ ¬
𝑋 ≺ 𝑋 |
22 | | 0ex 5175 |
. . . . 5
⊢ ∅
∈ V |
23 | | difeq2 4044 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅)) |
24 | | dif0 4286 |
. . . . . . 7
⊢ (𝑋 ∖ ∅) = 𝑋 |
25 | 23, 24 | eqtrdi 2849 |
. . . . . 6
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = 𝑋) |
26 | 25 | breq1d 5040 |
. . . . 5
⊢ (𝑦 = ∅ → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
27 | 22, 26 | sbcie 3760 |
. . . 4
⊢
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋) |
28 | 27 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
29 | 21, 28 | mtbiri 330 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ¬
[∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
30 | | simp1l 1194 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → 𝑋 ∈ dom card) |
31 | | difexg 5195 |
. . . . . 6
⊢ (𝑋 ∈ dom card → (𝑋 ∖ 𝑤) ∈ V) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑤) ∈ V) |
33 | | sscon 4066 |
. . . . . 6
⊢ (𝑤 ⊆ 𝑧 → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
34 | 33 | 3ad2ant3 1132 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
35 | | ssdomg 8538 |
. . . . 5
⊢ ((𝑋 ∖ 𝑤) ∈ V → ((𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤))) |
36 | 32, 34, 35 | sylc 65 |
. . . 4
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤)) |
37 | | domsdomtr 8636 |
. . . . 5
⊢ (((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ 𝑧) ≺ 𝑋) |
38 | 37 | ex 416 |
. . . 4
⊢ ((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
39 | 36, 38 | syl 17 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
40 | | vex 3444 |
. . . 4
⊢ 𝑤 ∈ V |
41 | | difeq2 4044 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑤)) |
42 | 41 | breq1d 5040 |
. . . 4
⊢ (𝑦 = 𝑤 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
43 | 40, 42 | sbcie 3760 |
. . 3
⊢
([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋) |
44 | | vex 3444 |
. . . 4
⊢ 𝑧 ∈ V |
45 | | difeq2 4044 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧)) |
46 | 45 | breq1d 5040 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋)) |
47 | 44, 46 | sbcie 3760 |
. . 3
⊢
([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋) |
48 | 39, 43, 47 | 3imtr4g 299 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 → [𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
49 | | infunsdom 9625 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
50 | 49 | ex 416 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋)) |
51 | | difindi 4208 |
. . . . . 6
⊢ (𝑋 ∖ (𝑧 ∩ 𝑤)) = ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) |
52 | 51 | breq1i 5037 |
. . . . 5
⊢ ((𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋 ↔ ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
53 | 50, 52 | syl6ibr 255 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
54 | 53 | 3ad2ant1 1130 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
55 | 47, 43 | anbi12i 629 |
. . 3
⊢
(([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) ↔ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
56 | 44 | inex1 5185 |
. . . 4
⊢ (𝑧 ∩ 𝑤) ∈ V |
57 | | difeq2 4044 |
. . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑧 ∩ 𝑤))) |
58 | 57 | breq1d 5040 |
. . . 4
⊢ (𝑦 = (𝑧 ∩ 𝑤) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
59 | 56, 58 | sbcie 3760 |
. . 3
⊢
([(𝑧 ∩
𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋) |
60 | 54, 55, 59 | 3imtr4g 299 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) → [(𝑧 ∩ 𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
61 | 7, 8, 20, 29, 48, 60 | isfild 22463 |
1
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ∈ (Fil‘𝑋)) |