Proof of Theorem isipodrs
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(Base‘(toInc‘𝐴)) = (Base‘(toInc‘𝐴)) |
| 2 | 1 | drsbn0 18350 |
. . . 4
⊢
((toInc‘𝐴)
∈ Dirset → (Base‘(toInc‘𝐴)) ≠ ∅) |
| 3 | 2 | neneqd 2945 |
. . 3
⊢
((toInc‘𝐴)
∈ Dirset → ¬ (Base‘(toInc‘𝐴)) = ∅) |
| 4 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(toInc‘𝐴) =
∅) |
| 5 | 4 | fveq2d 6910 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(Base‘(toInc‘𝐴)) = (Base‘∅)) |
| 6 | | base0 17252 |
. . . 4
⊢ ∅ =
(Base‘∅) |
| 7 | 5, 6 | eqtr4di 2795 |
. . 3
⊢ (¬
𝐴 ∈ V →
(Base‘(toInc‘𝐴)) = ∅) |
| 8 | 3, 7 | nsyl2 141 |
. 2
⊢
((toInc‘𝐴)
∈ Dirset → 𝐴
∈ V) |
| 9 | | simp1 1137 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧) → 𝐴 ∈ V) |
| 10 | | eqid 2737 |
. . . 4
⊢
(le‘(toInc‘𝐴)) = (le‘(toInc‘𝐴)) |
| 11 | 1, 10 | isdrs 18347 |
. . 3
⊢
((toInc‘𝐴)
∈ Dirset ↔ ((toInc‘𝐴) ∈ Proset ∧
(Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧))) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
(toInc‘𝐴) =
(toInc‘𝐴) |
| 13 | 12 | ipopos 18581 |
. . . . . . 7
⊢
(toInc‘𝐴)
∈ Poset |
| 14 | | posprs 18362 |
. . . . . . 7
⊢
((toInc‘𝐴)
∈ Poset → (toInc‘𝐴) ∈ Proset ) |
| 15 | 13, 14 | mp1i 13 |
. . . . . 6
⊢ (𝐴 ∈ V →
(toInc‘𝐴) ∈
Proset ) |
| 16 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ V → 𝐴 ∈ V) |
| 17 | 15, 16 | 2thd 265 |
. . . . 5
⊢ (𝐴 ∈ V →
((toInc‘𝐴) ∈
Proset ↔ 𝐴 ∈
V)) |
| 18 | 12 | ipobas 18576 |
. . . . . . 7
⊢ (𝐴 ∈ V → 𝐴 =
(Base‘(toInc‘𝐴))) |
| 19 | | neeq1 3003 |
. . . . . . . 8
⊢ (𝐴 =
(Base‘(toInc‘𝐴)) → (𝐴 ≠ ∅ ↔
(Base‘(toInc‘𝐴)) ≠ ∅)) |
| 20 | | rexeq 3322 |
. . . . . . . . . 10
⊢ (𝐴 =
(Base‘(toInc‘𝐴)) → (∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ ∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧))) |
| 21 | 20 | raleqbi1dv 3338 |
. . . . . . . . 9
⊢ (𝐴 =
(Base‘(toInc‘𝐴)) → (∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ ∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧))) |
| 22 | 21 | raleqbi1dv 3338 |
. . . . . . . 8
⊢ (𝐴 =
(Base‘(toInc‘𝐴)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ ∀𝑥 ∈ (Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧))) |
| 23 | 19, 22 | anbi12d 632 |
. . . . . . 7
⊢ (𝐴 =
(Base‘(toInc‘𝐴)) → ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ ((Base‘(toInc‘𝐴)) ≠ ∅ ∧
∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)))) |
| 24 | 18, 23 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ V → ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ ((Base‘(toInc‘𝐴)) ≠ ∅ ∧
∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)))) |
| 25 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝐴 ∈ V) |
| 26 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 27 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
| 28 | 12, 10 | ipole 18579 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑥(le‘(toInc‘𝐴))𝑧 ↔ 𝑥 ⊆ 𝑧)) |
| 29 | 25, 26, 27, 28 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑥(le‘(toInc‘𝐴))𝑧 ↔ 𝑥 ⊆ 𝑧)) |
| 30 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 31 | 12, 10 | ipole 18579 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ V ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑦(le‘(toInc‘𝐴))𝑧 ↔ 𝑦 ⊆ 𝑧)) |
| 32 | 25, 30, 27, 31 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑦(le‘(toInc‘𝐴))𝑧 ↔ 𝑦 ⊆ 𝑧)) |
| 33 | 29, 32 | anbi12d 632 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ (𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑧))) |
| 34 | | unss 4190 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑧) ↔ (𝑥 ∪ 𝑦) ⊆ 𝑧) |
| 35 | 33, 34 | bitrdi 287 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → ((𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ (𝑥 ∪ 𝑦) ⊆ 𝑧)) |
| 36 | 35 | rexbidva 3177 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) |
| 37 | 36 | 2ralbidva 3219 |
. . . . . . 7
⊢ (𝐴 ∈ V → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) |
| 38 | 37 | anbi2d 630 |
. . . . . 6
⊢ (𝐴 ∈ V → ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ (𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))) |
| 39 | 24, 38 | bitr3d 281 |
. . . . 5
⊢ (𝐴 ∈ V →
(((Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ (𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))) |
| 40 | 17, 39 | anbi12d 632 |
. . . 4
⊢ (𝐴 ∈ V →
(((toInc‘𝐴) ∈
Proset ∧ ((Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧))) ↔ (𝐴 ∈ V ∧ (𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)))) |
| 41 | | 3anass 1095 |
. . . 4
⊢
(((toInc‘𝐴)
∈ Proset ∧ (Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ ((toInc‘𝐴) ∈ Proset ∧
((Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)))) |
| 42 | | 3anass 1095 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧) ↔ (𝐴 ∈ V ∧ (𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))) |
| 43 | 40, 41, 42 | 3bitr4g 314 |
. . 3
⊢ (𝐴 ∈ V →
(((toInc‘𝐴) ∈
Proset ∧ (Base‘(toInc‘𝐴)) ≠ ∅ ∧ ∀𝑥 ∈
(Base‘(toInc‘𝐴))∀𝑦 ∈ (Base‘(toInc‘𝐴))∃𝑧 ∈ (Base‘(toInc‘𝐴))(𝑥(le‘(toInc‘𝐴))𝑧 ∧ 𝑦(le‘(toInc‘𝐴))𝑧)) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))) |
| 44 | 11, 43 | bitrid 283 |
. 2
⊢ (𝐴 ∈ V →
((toInc‘𝐴) ∈
Dirset ↔ (𝐴 ∈ V
∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))) |
| 45 | 8, 9, 44 | pm5.21nii 378 |
1
⊢
((toInc‘𝐴)
∈ Dirset ↔ (𝐴
∈ V ∧ 𝐴 ≠
∅ ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) |