| Step | Hyp | Ref
| Expression |
| 1 | | velsn 4642 |
. . . 4
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
| 2 | | eqimss 4042 |
. . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) |
| 3 | 2 | pm4.71ri 560 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
| 4 | 1, 3 | bitri 275 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
| 5 | 4 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴))) |
| 6 | | simpl 482 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ∈ 𝐵) |
| 7 | | eqid 2737 |
. . . 4
⊢ 𝐴 = 𝐴 |
| 8 | | eqsbc1 3835 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
| 9 | 7, 8 | mpbiri 258 |
. . 3
⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝑥 = 𝐴) |
| 10 | 9 | adantr 480 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → [𝐴 / 𝑥]𝑥 = 𝐴) |
| 11 | | simpr 484 |
. . . . 5
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
| 12 | 11 | necomd 2996 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ∅ ≠ 𝐴) |
| 13 | 12 | neneqd 2945 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ ∅ = 𝐴) |
| 14 | | 0ex 5307 |
. . . 4
⊢ ∅
∈ V |
| 15 | | eqsbc1 3835 |
. . . 4
⊢ (∅
∈ V → ([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴)) |
| 16 | 14, 15 | ax-mp 5 |
. . 3
⊢
([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴) |
| 17 | 13, 16 | sylnibr 329 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ [∅
/ 𝑥]𝑥 = 𝐴) |
| 18 | | sseq1 4009 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦)) |
| 19 | 18 | anbi2d 630 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦))) |
| 20 | | eqss 3999 |
. . . . . . 7
⊢ (𝑦 = 𝐴 ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦)) |
| 21 | 20 | biimpri 228 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦) → 𝑦 = 𝐴) |
| 22 | 19, 21 | biimtrdi 253 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → 𝑦 = 𝐴)) |
| 23 | 22 | com12 32 |
. . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
| 24 | 23 | 3adant1 1131 |
. . 3
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
| 25 | | sbcid 3805 |
. . 3
⊢
([𝑥 / 𝑥]𝑥 = 𝐴 ↔ 𝑥 = 𝐴) |
| 26 | | eqsbc1 3835 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
| 27 | 26 | elv 3485 |
. . 3
⊢
([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) |
| 28 | 24, 25, 27 | 3imtr4g 296 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → ([𝑥 / 𝑥]𝑥 = 𝐴 → [𝑦 / 𝑥]𝑥 = 𝐴)) |
| 29 | | ineq12 4215 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = (𝐴 ∩ 𝐴)) |
| 30 | | inidm 4227 |
. . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 31 | 29, 30 | eqtrdi 2793 |
. . . . 5
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
| 32 | 27, 25, 31 | syl2anb 598 |
. . . 4
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
| 33 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 34 | 33 | inex1 5317 |
. . . . 5
⊢ (𝑦 ∩ 𝑥) ∈ V |
| 35 | | eqsbc1 3835 |
. . . . 5
⊢ ((𝑦 ∩ 𝑥) ∈ V → ([(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴)) |
| 36 | 34, 35 | ax-mp 5 |
. . . 4
⊢
([(𝑦 ∩
𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴) |
| 37 | 32, 36 | sylibr 234 |
. . 3
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴) |
| 38 | 37 | a1i 11 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴) → (([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴)) |
| 39 | 5, 6, 10, 17, 28, 38 | isfild 23866 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴)) |