Step |
Hyp |
Ref |
Expression |
1 |
|
velsn |
⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 ) |
2 |
|
eqimss |
⊢ ( 𝑥 = 𝐴 → 𝑥 ⊆ 𝐴 ) |
3 |
2
|
pm4.71ri |
⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴 ) ) |
4 |
1 3
|
bitri |
⊢ ( 𝑥 ∈ { 𝐴 } ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴 ) ) |
5 |
4
|
a1i |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( 𝑥 ∈ { 𝐴 } ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝐴 ) ) ) |
6 |
|
simpl |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ 𝐵 ) |
7 |
|
eqid |
⊢ 𝐴 = 𝐴 |
8 |
|
eqsbc3 |
⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) ) |
9 |
7 8
|
mpbiri |
⊢ ( 𝐴 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 ) |
10 |
9
|
adantr |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 ) |
11 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ ) |
12 |
11
|
necomd |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∅ ≠ 𝐴 ) |
13 |
12
|
neneqd |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ¬ ∅ = 𝐴 ) |
14 |
|
0ex |
⊢ ∅ ∈ V |
15 |
|
eqsbc3 |
⊢ ( ∅ ∈ V → ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 ) ) |
16 |
14 15
|
ax-mp |
⊢ ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 ) |
17 |
13 16
|
sylnibr |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ¬ [ ∅ / 𝑥 ] 𝑥 = 𝐴 ) |
18 |
|
sseq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) ) |
19 |
18
|
anbi2d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) ) ) |
20 |
|
eqss |
⊢ ( 𝑦 = 𝐴 ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) ) |
21 |
20
|
biimpri |
⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) → 𝑦 = 𝐴 ) |
22 |
19 21
|
syl6bi |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → 𝑦 = 𝐴 ) ) |
23 |
22
|
com12 |
⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 = 𝐴 → 𝑦 = 𝐴 ) ) |
24 |
23
|
3adant1 |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 = 𝐴 → 𝑦 = 𝐴 ) ) |
25 |
|
sbcid |
⊢ ( [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝑥 = 𝐴 ) |
26 |
|
eqsbc3 |
⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) ) |
27 |
26
|
elv |
⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) |
28 |
24 25 27
|
3imtr4g |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → ( [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 → [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ) ) |
29 |
|
ineq12 |
⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑦 ∩ 𝑥 ) = ( 𝐴 ∩ 𝐴 ) ) |
30 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
31 |
29 30
|
eqtrdi |
⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑦 ∩ 𝑥 ) = 𝐴 ) |
32 |
27 25 31
|
syl2anb |
⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ∧ [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → ( 𝑦 ∩ 𝑥 ) = 𝐴 ) |
33 |
|
vex |
⊢ 𝑦 ∈ V |
34 |
33
|
inex1 |
⊢ ( 𝑦 ∩ 𝑥 ) ∈ V |
35 |
|
eqsbc3 |
⊢ ( ( 𝑦 ∩ 𝑥 ) ∈ V → ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦 ∩ 𝑥 ) = 𝐴 ) ) |
36 |
34 35
|
ax-mp |
⊢ ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦 ∩ 𝑥 ) = 𝐴 ) |
37 |
32 36
|
sylibr |
⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ∧ [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ) |
38 |
37
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ∧ [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ) ) |
39 |
5 6 10 17 28 38
|
isfild |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → { 𝐴 } ∈ ( Fil ‘ 𝐴 ) ) |