Step | Hyp | Ref
| Expression |
1 | | indthinc.b |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
2 | | prsthinc.h |
. 2
⊢ (𝜑 → ( ≤ ×
{1o}) = (Hom ‘𝐶)) |
3 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
4 | 3 | f1omo 45695 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
5 | | df-ov 7167 |
. . . . 5
⊢ (𝑥( ≤ ×
{1o})𝑦) = ((
≤
× {1o})‘〈𝑥, 𝑦〉) |
6 | 5 | eleq2i 2824 |
. . . 4
⊢ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ↔
𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
7 | 6 | mobii 2548 |
. . 3
⊢
(∃*𝑓 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ↔
∃*𝑓 𝑓 ∈ (( ≤ ×
{1o})‘〈𝑥, 𝑦〉)) |
8 | 4, 7 | sylibr 237 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑓 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦)) |
9 | | prsthinc.o |
. 2
⊢ (𝜑 → ∅ =
(comp‘𝐶)) |
10 | | prsthinc.p |
. 2
⊢ (𝜑 → 𝐶 ∈ Proset ) |
11 | | biid 264 |
. 2
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))) ↔
((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧)))) |
12 | | 0lt1o 8153 |
. . 3
⊢ ∅
∈ 1o |
13 | 1 | eleq2d 2818 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐶))) |
14 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) |
15 | | eqid 2738 |
. . . . . . . 8
⊢
(le‘𝐶) =
(le‘𝐶) |
16 | 14, 15 | prsref 17651 |
. . . . . . 7
⊢ ((𝐶 ∈ Proset ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦) |
17 | 10, 16 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦(le‘𝐶)𝑦) |
18 | 13, 17 | sylbida 595 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦(le‘𝐶)𝑦) |
19 | | prsthinc.l |
. . . . . . 7
⊢ (𝜑 → ≤ = (le‘𝐶)) |
20 | 19 | breqd 5038 |
. . . . . 6
⊢ (𝜑 → (𝑦 ≤ 𝑦 ↔ 𝑦(le‘𝐶)𝑦)) |
21 | 20 | biimpar 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦(le‘𝐶)𝑦) → 𝑦 ≤ 𝑦) |
22 | 18, 21 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ≤ 𝑦) |
23 | | eqidd 2739 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
24 | | 1oex 8137 |
. . . . . 6
⊢
1o ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1o ∈
V) |
26 | | 1n0 8143 |
. . . . . 6
⊢
1o ≠ ∅ |
27 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1o ≠
∅) |
28 | 23, 25, 27 | fvconstr 45690 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ≤ 𝑦 ↔ (𝑦( ≤ ×
{1o})𝑦) =
1o)) |
29 | 22, 28 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦( ≤ ×
{1o})𝑦) =
1o) |
30 | 12, 29 | eleqtrrid 2840 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∅ ∈ (𝑦( ≤ ×
{1o})𝑦)) |
31 | | 0ov 7201 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉∅𝑧) = ∅ |
32 | 31 | oveqi 7177 |
. . . . 5
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) = (𝑔∅𝑓) |
33 | | 0ov 7201 |
. . . . 5
⊢ (𝑔∅𝑓) = ∅ |
34 | 32, 33 | eqtri 2761 |
. . . 4
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) = ∅ |
35 | 34, 12 | eqeltri 2829 |
. . 3
⊢ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) ∈ 1o |
36 | | simpl 486 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝜑) |
37 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝐶 ∈ Proset
) |
38 | 1 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐶))) |
39 | 1 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝐶))) |
40 | 38, 13, 39 | 3anbi123d 1437 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)))) |
41 | 40 | biimpa 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) |
42 | 41 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥 ∈
(Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) |
43 | | eqidd 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ ( ≤ ×
{1o}) = ( ≤ ×
{1o})) |
44 | | simprrl 781 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦)) |
45 | 43, 44 | fvconstr2 45692 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥 ≤ 𝑦) |
46 | 19 | breqd 5038 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐶)𝑦)) |
47 | 46 | biimpd 232 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ≤ 𝑦 → 𝑥(le‘𝐶)𝑦)) |
48 | 36, 45, 47 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥(le‘𝐶)𝑦) |
49 | | simprrr 782 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧)) |
50 | 43, 49 | fvconstr2 45692 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑦 ≤ 𝑧) |
51 | 19 | breqd 5038 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐶)𝑧)) |
52 | 51 | biimpd 232 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ≤ 𝑧 → 𝑦(le‘𝐶)𝑧)) |
53 | 36, 50, 52 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑦(le‘𝐶)𝑧) |
54 | 14, 15 | prstr 17652 |
. . . . . 6
⊢ ((𝐶 ∈ Proset ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑥(le‘𝐶)𝑦 ∧ 𝑦(le‘𝐶)𝑧)) → 𝑥(le‘𝐶)𝑧) |
55 | 37, 42, 48, 53, 54 | syl112anc 1375 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ 𝑥(le‘𝐶)𝑧) |
56 | 19 | breqd 5038 |
. . . . . 6
⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐶)𝑧)) |
57 | 56 | biimprd 251 |
. . . . 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 45690 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥 ≤ 𝑧 ↔ (𝑥( ≤ ×
{1o})𝑧) =
1o)) |
62 | 58, 61 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑥( ≤ ×
{1o})𝑧) =
1o) |
63 | 35, 62 | eleqtrrid 2840 |
. 2
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥( ≤ ×
{1o})𝑦) ∧
𝑔 ∈ (𝑦( ≤ ×
{1o})𝑧))))
→ (𝑔(〈𝑥, 𝑦〉∅𝑧)𝑓) ∈ (𝑥( ≤ ×
{1o})𝑧)) |
64 | 1, 2, 8, 9, 10, 11, 30, 63 | isthincd2 45776 |
1
⊢ (𝜑 → (𝐶 ∈ ThinCat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ ∅))) |