Step | Hyp | Ref
| Expression |
1 | | velsn 4573 |
. . . 4
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
2 | | eqimss 4020 |
. . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) |
3 | 2 | pm4.71ri 561 |
. . . 4
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
4 | 1, 3 | bitri 276 |
. . 3
⊢ (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴)) |
5 | 4 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → (𝑥 ∈ {𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴))) |
6 | | elex 3510 |
. . 3
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) |
7 | 6 | adantr 481 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ∈ V) |
8 | | eqid 2818 |
. . . 4
⊢ 𝐴 = 𝐴 |
9 | | eqsbc3 3814 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐴 ↔ 𝐴 = 𝐴)) |
10 | 8, 9 | mpbiri 259 |
. . 3
⊢ (𝐴 ∈ 𝐵 → [𝐴 / 𝑥]𝑥 = 𝐴) |
11 | 10 | adantr 481 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → [𝐴 / 𝑥]𝑥 = 𝐴) |
12 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
13 | 12 | necomd 3068 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ∅ ≠ 𝐴) |
14 | 13 | neneqd 3018 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ ∅ = 𝐴) |
15 | | 0ex 5202 |
. . . 4
⊢ ∅
∈ V |
16 | | eqsbc3 3814 |
. . . 4
⊢ (∅
∈ V → ([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴)) |
17 | 15, 16 | ax-mp 5 |
. . 3
⊢
([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴) |
18 | 14, 17 | sylnibr 330 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → ¬ [∅
/ 𝑥]𝑥 = 𝐴) |
19 | | sseq1 3989 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦)) |
20 | 19 | anbi2d 628 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦))) |
21 | | eqss 3979 |
. . . . . . 7
⊢ (𝑦 = 𝐴 ↔ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦)) |
22 | 21 | biimpri 229 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦) → 𝑦 = 𝐴) |
23 | 20, 22 | syl6bi 254 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → 𝑦 = 𝐴)) |
24 | 23 | com12 32 |
. . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
25 | 24 | 3adant1 1122 |
. . 3
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
26 | | sbcid 3786 |
. . 3
⊢
([𝑥 / 𝑥]𝑥 = 𝐴 ↔ 𝑥 = 𝐴) |
27 | | eqsbc3 3814 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
28 | 27 | elv 3497 |
. . 3
⊢
([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) |
29 | 25, 26, 28 | 3imtr4g 297 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦) → ([𝑥 / 𝑥]𝑥 = 𝐴 → [𝑦 / 𝑥]𝑥 = 𝐴)) |
30 | | ineq12 4181 |
. . . . . 6
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = (𝐴 ∩ 𝐴)) |
31 | | inidm 4192 |
. . . . . 6
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
32 | 30, 31 | syl6eq 2869 |
. . . . 5
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
33 | 28, 26, 32 | syl2anb 597 |
. . . 4
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → (𝑦 ∩ 𝑥) = 𝐴) |
34 | | vex 3495 |
. . . . . 6
⊢ 𝑦 ∈ V |
35 | 34 | inex1 5212 |
. . . . 5
⊢ (𝑦 ∩ 𝑥) ∈ V |
36 | | eqsbc3 3814 |
. . . . 5
⊢ ((𝑦 ∩ 𝑥) ∈ V → ([(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴)) |
37 | 35, 36 | ax-mp 5 |
. . . 4
⊢
([(𝑦 ∩
𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦 ∩ 𝑥) = 𝐴) |
38 | 33, 37 | sylibr 235 |
. . 3
⊢
(([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴) |
39 | 38 | a1i 11 |
. 2
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴) → (([𝑦 / 𝑥]𝑥 = 𝐴 ∧ [𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦 ∩ 𝑥) / 𝑥]𝑥 = 𝐴)) |
40 | 5, 7, 11, 18, 29, 39 | isfild 22394 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴)) |