| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | difeq2 4120 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝑋 ∖ 𝑥) = (𝑋 ∖ 𝑦)) | 
| 2 | 1 | breq1d 5153 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝑋 ∖ 𝑥) ≺ 𝑋 ↔ (𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 3 | 2 | elrab 3692 | . . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 4 |  | velpw 4605 | . . . . 5
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) | 
| 5 | 4 | anbi1i 624 | . . . 4
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋) ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 6 | 3, 5 | bitri 275 | . . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 7 | 6 | a1i 11 | . 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ↔ (𝑦 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑦) ≺ 𝑋))) | 
| 8 |  | simpl 482 | . 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ∈ dom
card) | 
| 9 |  | difid 4376 | . . . 4
⊢ (𝑋 ∖ 𝑋) = ∅ | 
| 10 |  | infn0 9340 | . . . . . 6
⊢ (ω
≼ 𝑋 → 𝑋 ≠ ∅) | 
| 11 | 10 | adantl 481 | . . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → 𝑋 ≠ ∅) | 
| 12 |  | 0sdomg 9144 | . . . . . 6
⊢ (𝑋 ∈ dom card → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) | 
| 13 | 12 | adantr 480 | . . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (∅
≺ 𝑋 ↔ 𝑋 ≠ ∅)) | 
| 14 | 11, 13 | mpbird 257 | . . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ∅
≺ 𝑋) | 
| 15 | 9, 14 | eqbrtrid 5178 | . . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (𝑋 ∖ 𝑋) ≺ 𝑋) | 
| 16 |  | difeq2 4120 | . . . . . 6
⊢ (𝑦 = 𝑋 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑋)) | 
| 17 | 16 | breq1d 5153 | . . . . 5
⊢ (𝑦 = 𝑋 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) | 
| 18 | 17 | sbcieg 3828 | . . . 4
⊢ (𝑋 ∈ dom card →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) | 
| 19 | 18 | adantr 480 | . . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑋) ≺ 𝑋)) | 
| 20 | 15, 19 | mpbird 257 | . 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
[𝑋 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) | 
| 21 |  | sdomirr 9154 | . . 3
⊢  ¬
𝑋 ≺ 𝑋 | 
| 22 |  | 0ex 5307 | . . . . 5
⊢ ∅
∈ V | 
| 23 |  | difeq2 4120 | . . . . . . 7
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = (𝑋 ∖ ∅)) | 
| 24 |  | dif0 4378 | . . . . . . 7
⊢ (𝑋 ∖ ∅) = 𝑋 | 
| 25 | 23, 24 | eqtrdi 2793 | . . . . . 6
⊢ (𝑦 = ∅ → (𝑋 ∖ 𝑦) = 𝑋) | 
| 26 | 25 | breq1d 5153 | . . . . 5
⊢ (𝑦 = ∅ → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) | 
| 27 | 22, 26 | sbcie 3830 | . . . 4
⊢
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋) | 
| 28 | 27 | a1i 11 | . . 3
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) →
([∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋)) | 
| 29 | 21, 28 | mtbiri 327 | . 2
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → ¬
[∅ / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) | 
| 30 |  | simp1l 1198 | . . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → 𝑋 ∈ dom card) | 
| 31 | 30 | difexd 5331 | . . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑤) ∈ V) | 
| 32 |  | sscon 4143 | . . . . . 6
⊢ (𝑤 ⊆ 𝑧 → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) | 
| 33 | 32 | 3ad2ant3 1136 | . . . . 5
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤)) | 
| 34 |  | ssdomg 9040 | . . . . 5
⊢ ((𝑋 ∖ 𝑤) ∈ V → ((𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑤) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤))) | 
| 35 | 31, 33, 34 | sylc 65 | . . . 4
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → (𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤)) | 
| 36 |  | domsdomtr 9152 | . . . . 5
⊢ (((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ 𝑧) ≺ 𝑋) | 
| 37 | 36 | ex 412 | . . . 4
⊢ ((𝑋 ∖ 𝑧) ≼ (𝑋 ∖ 𝑤) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) | 
| 38 | 35, 37 | syl 17 | . . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ((𝑋 ∖ 𝑤) ≺ 𝑋 → (𝑋 ∖ 𝑧) ≺ 𝑋)) | 
| 39 |  | vex 3484 | . . . 4
⊢ 𝑤 ∈ V | 
| 40 |  | difeq2 4120 | . . . . 5
⊢ (𝑦 = 𝑤 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑤)) | 
| 41 | 40 | breq1d 5153 | . . . 4
⊢ (𝑦 = 𝑤 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋)) | 
| 42 | 39, 41 | sbcie 3830 | . . 3
⊢
([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑤) ≺ 𝑋) | 
| 43 |  | vex 3484 | . . . 4
⊢ 𝑧 ∈ V | 
| 44 |  | difeq2 4120 | . . . . 5
⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧)) | 
| 45 | 44 | breq1d 5153 | . . . 4
⊢ (𝑦 = 𝑧 → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋)) | 
| 46 | 43, 45 | sbcie 3830 | . . 3
⊢
([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ 𝑧) ≺ 𝑋) | 
| 47 | 38, 42, 46 | 3imtr4g 296 | . 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 → [𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 48 |  | infunsdom 10253 | . . . . . 6
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) | 
| 49 | 48 | ex 412 | . . . . 5
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋)) | 
| 50 |  | difindi 4292 | . . . . . 6
⊢ (𝑋 ∖ (𝑧 ∩ 𝑤)) = ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) | 
| 51 | 50 | breq1i 5150 | . . . . 5
⊢ ((𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋 ↔ ((𝑋 ∖ 𝑧) ∪ (𝑋 ∖ 𝑤)) ≺ 𝑋) | 
| 52 | 49, 51 | imbitrrdi 252 | . . . 4
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) | 
| 53 | 52 | 3ad2ant1 1134 | . . 3
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋) → (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) | 
| 54 | 46, 42 | anbi12i 628 | . . 3
⊢
(([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) ↔ ((𝑋 ∖ 𝑧) ≺ 𝑋 ∧ (𝑋 ∖ 𝑤) ≺ 𝑋)) | 
| 55 | 43 | inex1 5317 | . . . 4
⊢ (𝑧 ∩ 𝑤) ∈ V | 
| 56 |  | difeq2 4120 | . . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝑋 ∖ 𝑦) = (𝑋 ∖ (𝑧 ∩ 𝑤))) | 
| 57 | 56 | breq1d 5153 | . . . 4
⊢ (𝑦 = (𝑧 ∩ 𝑤) → ((𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋)) | 
| 58 | 55, 57 | sbcie 3830 | . . 3
⊢
([(𝑧 ∩
𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ↔ (𝑋 ∖ (𝑧 ∩ 𝑤)) ≺ 𝑋) | 
| 59 | 53, 54, 58 | 3imtr4g 296 | . 2
⊢ (((𝑋 ∈ dom card ∧ ω
≼ 𝑋) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (([𝑧 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋 ∧ [𝑤 / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋) → [(𝑧 ∩ 𝑤) / 𝑦](𝑋 ∖ 𝑦) ≺ 𝑋)) | 
| 60 | 7, 8, 20, 29, 47, 59 | isfild 23866 | 1
⊢ ((𝑋 ∈ dom card ∧ ω
≼ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ∈ (Fil‘𝑋)) |