Step | Hyp | Ref
| Expression |
1 | | 0ex 5026 |
. . . . 5
⊢ ∅
∈ V |
2 | 1 | eldm 5566 |
. . . 4
⊢ (∅
∈ dom 𝐹 ↔
∃𝑦∅𝐹𝑦) |
3 | | brtpos0 7641 |
. . . . . . 7
⊢ (𝑦 ∈ V → (∅tpos
𝐹𝑦 ↔ ∅𝐹𝑦)) |
4 | 3 | elv 3402 |
. . . . . 6
⊢
(∅tpos 𝐹𝑦 ↔ ∅𝐹𝑦) |
5 | | 0nelxp 5389 |
. . . . . . . 8
⊢ ¬
∅ ∈ (V × V) |
6 | | df-rel 5362 |
. . . . . . . . 9
⊢ (Rel dom
tpos 𝐹 ↔ dom tpos
𝐹 ⊆ (V ×
V)) |
7 | | ssel 3815 |
. . . . . . . . 9
⊢ (dom tpos
𝐹 ⊆ (V × V)
→ (∅ ∈ dom tpos 𝐹 → ∅ ∈ (V ×
V))) |
8 | 6, 7 | sylbi 209 |
. . . . . . . 8
⊢ (Rel dom
tpos 𝐹 → (∅
∈ dom tpos 𝐹 →
∅ ∈ (V × V))) |
9 | 5, 8 | mtoi 191 |
. . . . . . 7
⊢ (Rel dom
tpos 𝐹 → ¬ ∅
∈ dom tpos 𝐹) |
10 | | vex 3401 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
11 | 1, 10 | breldm 5574 |
. . . . . . 7
⊢
(∅tpos 𝐹𝑦 → ∅ ∈ dom tpos
𝐹) |
12 | 9, 11 | nsyl3 136 |
. . . . . 6
⊢
(∅tpos 𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
13 | 4, 12 | sylbir 227 |
. . . . 5
⊢
(∅𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
14 | 13 | exlimiv 1973 |
. . . 4
⊢
(∃𝑦∅𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
15 | 2, 14 | sylbi 209 |
. . 3
⊢ (∅
∈ dom 𝐹 → ¬
Rel dom tpos 𝐹) |
16 | 15 | con2i 137 |
. 2
⊢ (Rel dom
tpos 𝐹 → ¬ ∅
∈ dom 𝐹) |
17 | | vex 3401 |
. . . . . 6
⊢ 𝑥 ∈ V |
18 | 17 | eldm 5566 |
. . . . 5
⊢ (𝑥 ∈ dom tpos 𝐹 ↔ ∃𝑦 𝑥tpos 𝐹𝑦) |
19 | | relcnv 5757 |
. . . . . . . . . . 11
⊢ Rel ◡dom 𝐹 |
20 | | df-rel 5362 |
. . . . . . . . . . 11
⊢ (Rel
◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V)) |
21 | 19, 20 | mpbi 222 |
. . . . . . . . . 10
⊢ ◡dom 𝐹 ⊆ (V × V) |
22 | 21 | sseli 3817 |
. . . . . . . . 9
⊢ (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V)) |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V))) |
24 | | elsni 4415 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
25 | 24 | breq1d 4896 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 ↔ ∅tpos 𝐹𝑦)) |
26 | 1, 10 | breldm 5574 |
. . . . . . . . . . . . 13
⊢
(∅𝐹𝑦 → ∅ ∈ dom 𝐹) |
27 | 26 | pm2.24d 149 |
. . . . . . . . . . . 12
⊢
(∅𝐹𝑦 → (¬ ∅ ∈
dom 𝐹 → 𝑥 ∈ (V ×
V))) |
28 | 4, 27 | sylbi 209 |
. . . . . . . . . . 11
⊢
(∅tpos 𝐹𝑦 → (¬ ∅ ∈
dom 𝐹 → 𝑥 ∈ (V ×
V))) |
29 | 25, 28 | syl6bi 245 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ (V × V)))) |
30 | 29 | com3l 89 |
. . . . . . . . 9
⊢ (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V)))) |
31 | 30 | impcom 398 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V))) |
32 | | brtpos2 7640 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V → (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦))) |
33 | 32 | elv 3402 |
. . . . . . . . . . 11
⊢ (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦)) |
34 | 33 | simplbi 493 |
. . . . . . . . . 10
⊢ (𝑥tpos 𝐹𝑦 → 𝑥 ∈ (◡dom 𝐹 ∪ {∅})) |
35 | | elun 3976 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↔ (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
36 | 34, 35 | sylib 210 |
. . . . . . . . 9
⊢ (𝑥tpos 𝐹𝑦 → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
37 | 36 | adantl 475 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
38 | 23, 31, 37 | mpjaod 849 |
. . . . . . 7
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → 𝑥 ∈ (V × V)) |
39 | 38 | ex 403 |
. . . . . 6
⊢ (¬
∅ ∈ dom 𝐹 →
(𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V))) |
40 | 39 | exlimdv 1976 |
. . . . 5
⊢ (¬
∅ ∈ dom 𝐹 →
(∃𝑦 𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V))) |
41 | 18, 40 | syl5bi 234 |
. . . 4
⊢ (¬
∅ ∈ dom 𝐹 →
(𝑥 ∈ dom tpos 𝐹 → 𝑥 ∈ (V × V))) |
42 | 41 | ssrdv 3827 |
. . 3
⊢ (¬
∅ ∈ dom 𝐹 →
dom tpos 𝐹 ⊆ (V
× V)) |
43 | 42, 6 | sylibr 226 |
. 2
⊢ (¬
∅ ∈ dom 𝐹 →
Rel dom tpos 𝐹) |
44 | 16, 43 | impbii 201 |
1
⊢ (Rel dom
tpos 𝐹 ↔ ¬ ∅
∈ dom 𝐹) |