Step | Hyp | Ref
| Expression |
1 | | velsn 4577 |
. . . 4
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
2 | | eqimss 3977 |
. . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) |
3 | 2 | pm4.71ri 561 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
4 | 1, 3 | bitri 274 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
5 | 4 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴))) |
6 | | simpl 483 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ∈ 𝐵) |
7 | | eqid 2738 |
. . . 4
⊢ 𝐴 = 𝐴 |
8 | | eqsbc1 3765 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
9 | 7, 8 | mpbiri 257 |
. . 3
⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝑥 = 𝐴) |
10 | 9 | adantr 481 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → [𝐴 / 𝑥]𝑥 = 𝐴) |
11 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
12 | 11 | necomd 2999 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ∅ ≠ 𝐴) |
13 | 12 | neneqd 2948 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ ∅ = 𝐴) |
14 | | 0ex 5231 |
. . . 4
⊢ ∅
∈ V |
15 | | eqsbc1 3765 |
. . . 4
⊢ (∅
∈ V → ([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴)) |
16 | 14, 15 | ax-mp 5 |
. . 3
⊢
([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴) |
17 | 13, 16 | sylnibr 329 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ [∅
/ 𝑥]𝑥 = 𝐴) |
18 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦)) |
19 | 18 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦))) |
20 | | eqss 3936 |
. . . . . . 7
⊢ (𝑦 = 𝐴 ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦)) |
21 | 20 | biimpri 227 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦) → 𝑦 = 𝐴) |
22 | 19, 21 | syl6bi 252 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → 𝑦 = 𝐴)) |
23 | 22 | com12 32 |
. . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
24 | 23 | 3adant1 1129 |
. . 3
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
25 | | sbcid 3733 |
. . 3
⊢
([𝑥 / 𝑥]𝑥 = 𝐴 ↔ 𝑥 = 𝐴) |
26 | | eqsbc1 3765 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
27 | 26 | elv 3438 |
. . 3
⊢
([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) |
28 | 24, 25, 27 | 3imtr4g 296 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → ([𝑥 / 𝑥]𝑥 = 𝐴 → [𝑦 / 𝑥]𝑥 = 𝐴)) |
29 | | ineq12 4141 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = (𝐴 ∩ 𝐴)) |
30 | | inidm 4152 |
. . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
31 | 29, 30 | eqtrdi 2794 |
. . . . 5
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
32 | 27, 25, 31 | syl2anb 598 |
. . . 4
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
33 | | vex 3436 |
. . . . . 6
⊢ 𝑦 ∈ V |
34 | 33 | inex1 5241 |
. . . . 5
⊢ (𝑦 ∩ 𝑥) ∈ V |
35 | | eqsbc1 3765 |
. . . . 5
⊢ ((𝑦 ∩ 𝑥) ∈ V → ([(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴)) |
36 | 34, 35 | ax-mp 5 |
. . . 4
⊢
([(𝑦 ∩
𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴) |
37 | 32, 36 | sylibr 233 |
. . 3
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴) |
38 | 37 | a1i 11 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴) → (([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴)) |
39 | 5, 6, 10, 17, 28, 38 | isfild 23009 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴)) |