Step | Hyp | Ref
| Expression |
1 | | difeq2 4051 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑋 ∖ 𝑥) = (𝑋 ∖ 𝑦)) |
2 | 1 | breq1d 5084 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑋 ∖ 𝑥) ≺ 𝑋 ↔ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
3 | 2 | elrab 3624 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
4 | | velpw 4538 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
5 | 4 | anbi1i 624 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋) ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
6 | 3, 5 | bitri 274 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋))) |
8 | | simpl 483 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ∈ dom
card) |
9 | | difid 4304 |
. . . 4
⊢ (𝑋 ∖ 𝑋) = ∅ |
10 | | infn0 9076 |
. . . . . 6
⊢ (ω
≼ 𝑋 → 𝑋 ≠ ∅) |
11 | 10 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ≠ ∅) |
12 | | 0sdomg 8891 |
. . . . . 6
⊢ (𝑋 ∈ dom card → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
13 | 12 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) |
14 | 11, 13 | mpbird 256 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ∅
≺ 𝑋) |
15 | 9, 14 | eqbrtrid 5109 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑋 ∖ 𝑋) ≺ 𝑋) |
16 | | difeq2 4051 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋)) |
17 | 16 | breq1d 5084 |
. . . . 5
⊢ (𝑦 = 𝑋 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
18 | 17 | sbcieg 3756 |
. . . 4
⊢ (𝑋 ∈ dom card →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
19 | 18 | adantr 481 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) |
20 | 15, 19 | mpbird 256 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
[𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
21 | | sdomirr 8901 |
. . 3
⊢ ¬
𝑋 ≺ 𝑋 |
22 | | 0ex 5231 |
. . . . 5
⊢ ∅
∈ V |
23 | | difeq2 4051 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅)) |
24 | | dif0 4306 |
. . . . . . 7
⊢ (𝑋 ∖ ∅) = 𝑋 |
25 | 23, 24 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = 𝑋) |
26 | 25 | breq1d 5084 |
. . . . 5
⊢ (𝑦 = ∅ → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
27 | 22, 26 | sbcie 3759 |
. . . 4
⊢
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋) |
28 | 27 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) |
29 | 21, 28 | mtbiri 327 |
. 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ¬
[∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) |
30 | | simp1l 1196 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → 𝑋 ∈ dom card) |
31 | 30 | difexd 5253 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑤) ∈ V) |
32 | | sscon 4073 |
. . . . . 6
⊢ (𝑤 ⊆ 𝑧 → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
33 | 32 | 3ad2ant3 1134 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) |
34 | | ssdomg 8786 |
. . . . 5
⊢ ((𝑋 ∖ 𝑤) ∈ V → ((𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤))) |
35 | 31, 33, 34 | sylc 65 |
. . . 4
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤)) |
36 | | domsdomtr 8899 |
. . . . 5
⊢ (((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ 𝑧) ≺ 𝑋) |
37 | 36 | ex 413 |
. . . 4
⊢ ((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
38 | 35, 37 | syl 17 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) |
39 | | vex 3436 |
. . . 4
⊢ 𝑤 ∈ V |
40 | | difeq2 4051 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑤)) |
41 | 40 | breq1d 5084 |
. . . 4
⊢ (𝑦 = 𝑤 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
42 | 39, 41 | sbcie 3759 |
. . 3
⊢
([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋) |
43 | | vex 3436 |
. . . 4
⊢ 𝑧 ∈ V |
44 | | difeq2 4051 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧)) |
45 | 44 | breq1d 5084 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋)) |
46 | 43, 45 | sbcie 3759 |
. . 3
⊢
([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋) |
47 | 38, 42, 46 | 3imtr4g 296 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 → [𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
48 | | infunsdom 9970 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
49 | 48 | ex 413 |
. . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋)) |
50 | | difindi 4215 |
. . . . . 6
⊢ (𝑋 ∖ (𝑧 ∩ 𝑤)) = ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) |
51 | 50 | breq1i 5081 |
. . . . 5
⊢ ((𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋 ↔ ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) |
52 | 49, 51 | syl6ibr 251 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
53 | 52 | 3ad2ant1 1132 |
. . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
54 | 46, 42 | anbi12i 627 |
. . 3
⊢
(([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) ↔ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) |
55 | 43 | inex1 5241 |
. . . 4
⊢ (𝑧 ∩ 𝑤) ∈ V |
56 | | difeq2 4051 |
. . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑧 ∩ 𝑤))) |
57 | 56 | breq1d 5084 |
. . . 4
⊢ (𝑦 = (𝑧 ∩ 𝑤) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) |
58 | 55, 57 | sbcie 3759 |
. . 3
⊢
([(𝑧 ∩
𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋) |
59 | 53, 54, 58 | 3imtr4g 296 |
. 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) → [(𝑧 ∩ 𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) |
60 | 7, 8, 20, 29, 47, 59 | isfild 23009 |
1
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ∈ (Fil‘𝑋)) |