| Step | Hyp | Ref
| Expression |
| 1 | | indthinc.b |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
| 2 | | prsthinc.h |
. 2
⊢ (𝜑 → ( ≤ ×
{1o}) = (Hom ‘𝐶)) |
| 3 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
| 4 | 3 | f1omo 48792 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
| 5 | | df-ov 7434 |
. . . . 5
⊢ (𝑥( ≤ ×
{1o})𝑦) = ((
≤
× {1o})‘〈𝑥, 𝑦〉) |
| 6 | 5 | eleq2i 2833 |
. . . 4
⊢ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ↔
𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
| 7 | 6 | mobii 2548 |
. . 3
⊢
(∃*𝑓 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ↔
∃*𝑓 𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
| 8 | 4, 7 | sylibr 234 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦)) |
| 9 | | prsthinc.o |
. 2
⊢ (𝜑 → ∅ =
(comp‘𝐶)) |
| 10 | | prsthinc.p |
. 2
⊢ (𝜑 → 𝐶 ∈ Proset ) |
| 11 | | biid 261 |
. 2
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))) ↔
((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧)))) |
| 12 | | 0lt1o 8542 |
. . 3
⊢ ∅
∈ 1o |
| 13 | 1 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐶))) |
| 14 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢
(le‘𝐶) =
(le‘𝐶) |
| 16 | 14, 15 | prsref 18344 |
. . . . . . 7
⊢ ((𝐶 ∈ Proset ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦) |
| 17 | 10, 16 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦) |
| 18 | 13, 17 | sylbida 592 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦(le‘𝐶)𝑦) |
| 19 | | prsthinc.l |
. . . . . . 7
⊢ (𝜑 → ≤ = (le‘𝐶)) |
| 20 | 19 | breqd 5154 |
. . . . . 6
⊢ (𝜑 → (𝑦 ≤ 𝑦 ↔ 𝑦(le‘𝐶)𝑦)) |
| 21 | 20 | biimpar 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦(le‘𝐶)𝑦) → 𝑦 ≤ 𝑦) |
| 22 | 18, 21 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ≤ 𝑦) |
| 23 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
| 24 | | 1oex 8516 |
. . . . . 6
⊢
1o ∈ V |
| 25 | 24 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1o ∈
V) |
| 26 | | 1n0 8526 |
. . . . . 6
⊢
1o ≠ ∅ |
| 27 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1o ≠
∅) |
| 28 | 23, 25, 27 | fvconstr 48765 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ≤ 𝑦 ↔ (𝑦( ≤ ×
{1o})𝑦) =
1o)) |
| 29 | 22, 28 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦( ≤ ×
{1o})𝑦) =
1o) |
| 30 | 12, 29 | eleqtrrid 2848 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∅ ∈ (𝑦( ≤ ×
{1o})𝑦)) |
| 31 | | 0ov 7468 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉∅𝑧) = ∅ |
| 32 | 31 | oveqi 7444 |
. . . . 5
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) = (𝑔∅𝑓) |
| 33 | | 0ov 7468 |
. . . . 5
⊢ (𝑔∅𝑓) = ∅ |
| 34 | 32, 33 | eqtri 2765 |
. . . 4
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) = ∅ |
| 35 | 34, 12 | eqeltri 2837 |
. . 3
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) ∈ 1o |
| 36 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝜑) |
| 37 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝐶 ∈ Proset
) |
| 38 | 1 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐶))) |
| 39 | 1 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝐶))) |
| 40 | 38, 13, 39 | 3anbi123d 1438 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))) |
| 41 | 40 | biimpa 476 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) |
| 42 | 41 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥 ∈
(Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) |
| 43 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
| 44 | | simprrl 781 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦)) |
| 45 | 43, 44 | fvconstr2 48767 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥 ≤ 𝑦) |
| 46 | 19 | breqd 5154 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐶)𝑦)) |
| 47 | 46 | biimpd 229 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ≤ 𝑦 → 𝑥(le‘𝐶)𝑦)) |
| 48 | 36, 45, 47 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥(le‘𝐶)𝑦) |
| 49 | | simprrr 782 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧)) |
| 50 | 43, 49 | fvconstr2 48767 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑦 ≤ 𝑧) |
| 51 | 19 | breqd 5154 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐶)𝑧)) |
| 52 | 51 | biimpd 229 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ≤ 𝑧 → 𝑦(le‘𝐶)𝑧)) |
| 53 | 36, 50, 52 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑦(le‘𝐶)𝑧) |
| 54 | 14, 15 | prstr 18345 |
. . . . . 6
⊢ ((𝐶 ∈ Proset ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑥(le‘𝐶)𝑦 ∧ 𝑦(le‘𝐶)𝑧)) → 𝑥(le‘𝐶)𝑧) |
| 55 | 37, 42, 48, 53, 54 | syl112anc 1376 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥(le‘𝐶)𝑧) |
| 56 | 19 | breqd 5154 |
. . . . . 6
⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐶)𝑧)) |
| 57 | 56 | biimprd 248 |
. . . . 5
⊢ (𝜑 → (𝑥(le‘𝐶)𝑧 → 𝑥 ≤ 𝑧)) |
| 58 | 36, 55, 57 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥 ≤ 𝑧) |
| 59 | 24 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 1o ∈ V) |
| 60 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 1o ≠ ∅) |
| 61 | 43, 59, 60 | fvconstr 48765 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥 ≤ 𝑧 ↔ (𝑥( ≤ ×
{1o})𝑧) =
1o)) |
| 62 | 58, 61 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥( ≤ ×
{1o})𝑧) =
1o) |
| 63 | 35, 62 | eleqtrrid 2848 |
. 2
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) ∈ (𝑥( ≤ ×
{1o})𝑧)) |
| 64 | 1, 2, 8, 9, 10, 11, 30, 63 | isthincd2 49086 |
1
⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) |