Step |
Hyp |
Ref |
Expression |
1 |
|
brtpos2 |
⊢ ( 𝐴 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐴 ↔ ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) ) ) |
2 |
|
ssun2 |
⊢ { ∅ } ⊆ ( ◡ dom 𝐹 ∪ { ∅ } ) |
3 |
|
0ex |
⊢ ∅ ∈ V |
4 |
3
|
snid |
⊢ ∅ ∈ { ∅ } |
5 |
2 4
|
sselii |
⊢ ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) |
6 |
5
|
biantrur |
⊢ ( ∪ ◡ { ∅ } 𝐹 𝐴 ↔ ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) ) |
7 |
|
cnvsn0 |
⊢ ◡ { ∅ } = ∅ |
8 |
7
|
unieqi |
⊢ ∪ ◡ { ∅ } = ∪ ∅ |
9 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
10 |
8 9
|
eqtri |
⊢ ∪ ◡ { ∅ } = ∅ |
11 |
10
|
breq1i |
⊢ ( ∪ ◡ { ∅ } 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 ) |
12 |
6 11
|
bitr3i |
⊢ ( ( ∅ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ∅ } 𝐹 𝐴 ) ↔ ∅ 𝐹 𝐴 ) |
13 |
1 12
|
bitrdi |
⊢ ( 𝐴 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐴 ↔ ∅ 𝐹 𝐴 ) ) |