Step | Hyp | Ref
| Expression |
1 | | 0ex 3884 |
. . . . 5
⊢ ∅
∈ V |
2 | 1 | eldm 4532 |
. . . 4
⊢ (∅
∈ dom 𝐹 ↔
∃𝑦∅𝐹𝑦) |
3 | | vex 2560 |
. . . . . . 7
⊢ 𝑦 ∈ V |
4 | | brtpos0 5867 |
. . . . . . 7
⊢ (𝑦 ∈ V → (∅tpos
𝐹𝑦 ↔ ∅𝐹𝑦)) |
5 | 3, 4 | ax-mp 7 |
. . . . . 6
⊢
(∅tpos 𝐹𝑦 ↔ ∅𝐹𝑦) |
6 | | 0nelxp 4372 |
. . . . . . . 8
⊢ ¬
∅ ∈ (V × V) |
7 | | df-rel 4352 |
. . . . . . . . 9
⊢ (Rel dom
tpos 𝐹 ↔ dom tpos
𝐹 ⊆ (V ×
V)) |
8 | | ssel 2939 |
. . . . . . . . 9
⊢ (dom tpos
𝐹 ⊆ (V × V)
→ (∅ ∈ dom tpos 𝐹 → ∅ ∈ (V ×
V))) |
9 | 7, 8 | sylbi 114 |
. . . . . . . 8
⊢ (Rel dom
tpos 𝐹 → (∅
∈ dom tpos 𝐹 →
∅ ∈ (V × V))) |
10 | 6, 9 | mtoi 590 |
. . . . . . 7
⊢ (Rel dom
tpos 𝐹 → ¬ ∅
∈ dom tpos 𝐹) |
11 | 1, 3 | breldm 4539 |
. . . . . . 7
⊢
(∅tpos 𝐹𝑦 → ∅ ∈ dom tpos
𝐹) |
12 | 10, 11 | nsyl3 556 |
. . . . . 6
⊢
(∅tpos 𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
13 | 5, 12 | sylbir 125 |
. . . . 5
⊢
(∅𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
14 | 13 | exlimiv 1489 |
. . . 4
⊢
(∃𝑦∅𝐹𝑦 → ¬ Rel dom tpos 𝐹) |
15 | 2, 14 | sylbi 114 |
. . 3
⊢ (∅
∈ dom 𝐹 → ¬
Rel dom tpos 𝐹) |
16 | 15 | con2i 557 |
. 2
⊢ (Rel dom
tpos 𝐹 → ¬ ∅
∈ dom 𝐹) |
17 | | vex 2560 |
. . . . . 6
⊢ 𝑥 ∈ V |
18 | 17 | eldm 4532 |
. . . . 5
⊢ (𝑥 ∈ dom tpos 𝐹 ↔ ∃𝑦 𝑥tpos 𝐹𝑦) |
19 | | relcnv 4703 |
. . . . . . . . . . 11
⊢ Rel ◡dom 𝐹 |
20 | | df-rel 4352 |
. . . . . . . . . . 11
⊢ (Rel
◡dom 𝐹 ↔ ◡dom 𝐹 ⊆ (V × V)) |
21 | 19, 20 | mpbi 133 |
. . . . . . . . . 10
⊢ ◡dom 𝐹 ⊆ (V × V) |
22 | 21 | sseli 2941 |
. . . . . . . . 9
⊢ (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V)) |
23 | 22 | a1i 9 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 → 𝑥 ∈ (V × V))) |
24 | | elsni 3393 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
25 | 24 | breq1d 3774 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 ↔ ∅tpos 𝐹𝑦)) |
26 | 1, 3 | breldm 4539 |
. . . . . . . . . . . . 13
⊢
(∅𝐹𝑦 → ∅ ∈ dom 𝐹) |
27 | 26 | pm2.24d 552 |
. . . . . . . . . . . 12
⊢
(∅𝐹𝑦 → (¬ ∅ ∈
dom 𝐹 → 𝑥 ∈ (V ×
V))) |
28 | 5, 27 | sylbi 114 |
. . . . . . . . . . 11
⊢
(∅tpos 𝐹𝑦 → (¬ ∅ ∈
dom 𝐹 → 𝑥 ∈ (V ×
V))) |
29 | 25, 28 | syl6bi 152 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅} → (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → 𝑥 ∈ (V × V)))) |
30 | 29 | com3l 75 |
. . . . . . . . 9
⊢ (𝑥tpos 𝐹𝑦 → (¬ ∅ ∈ dom 𝐹 → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V)))) |
31 | 30 | impcom 116 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ {∅} → 𝑥 ∈ (V × V))) |
32 | | brtpos2 5866 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V → (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦))) |
33 | 3, 32 | ax-mp 7 |
. . . . . . . . . . 11
⊢ (𝑥tpos 𝐹𝑦 ↔ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝑥}𝐹𝑦)) |
34 | 33 | simplbi 259 |
. . . . . . . . . 10
⊢ (𝑥tpos 𝐹𝑦 → 𝑥 ∈ (◡dom 𝐹 ∪ {∅})) |
35 | | elun 3084 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↔ (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
36 | 34, 35 | sylib 127 |
. . . . . . . . 9
⊢ (𝑥tpos 𝐹𝑦 → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
37 | 36 | adantl 262 |
. . . . . . . 8
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → (𝑥 ∈ ◡dom 𝐹 ∨ 𝑥 ∈ {∅})) |
38 | 23, 31, 37 | mpjaod 638 |
. . . . . . 7
⊢ ((¬
∅ ∈ dom 𝐹 ∧
𝑥tpos 𝐹𝑦) → 𝑥 ∈ (V × V)) |
39 | 38 | ex 108 |
. . . . . 6
⊢ (¬
∅ ∈ dom 𝐹 →
(𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V))) |
40 | 39 | exlimdv 1700 |
. . . . 5
⊢ (¬
∅ ∈ dom 𝐹 →
(∃𝑦 𝑥tpos 𝐹𝑦 → 𝑥 ∈ (V × V))) |
41 | 18, 40 | syl5bi 141 |
. . . 4
⊢ (¬
∅ ∈ dom 𝐹 →
(𝑥 ∈ dom tpos 𝐹 → 𝑥 ∈ (V × V))) |
42 | 41 | ssrdv 2951 |
. . 3
⊢ (¬
∅ ∈ dom 𝐹 →
dom tpos 𝐹 ⊆ (V
× V)) |
43 | 42, 7 | sylibr 137 |
. 2
⊢ (¬
∅ ∈ dom 𝐹 →
Rel dom tpos 𝐹) |
44 | 16, 43 | impbii 117 |
1
⊢ (Rel dom
tpos 𝐹 ↔ ¬ ∅
∈ dom 𝐹) |