Step |
Hyp |
Ref |
Expression |
1 |
|
isprs.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
isprs.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) ) |
4 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ( le ‘ 𝐾 ) ) |
5 |
4
|
sbceq1d |
⊢ ( 𝑓 = 𝐾 → ( [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
6 |
3 5
|
sbceqbid |
⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
7 |
|
fvex |
⊢ ( Base ‘ 𝐾 ) ∈ V |
8 |
|
fvex |
⊢ ( le ‘ 𝐾 ) ∈ V |
9 |
|
eqtr3 |
⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝐵 = ( Base ‘ 𝐾 ) ) → 𝑏 = 𝐵 ) |
10 |
1 9
|
mpan2 |
⊢ ( 𝑏 = ( Base ‘ 𝐾 ) → 𝑏 = 𝐵 ) |
11 |
|
raleq |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
12 |
11
|
raleqbi1dv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
13 |
12
|
raleqbi1dv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
14 |
10 13
|
syl |
⊢ ( 𝑏 = ( Base ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) ) |
15 |
|
eqtr3 |
⊢ ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ≤ = ( le ‘ 𝐾 ) ) → 𝑟 = ≤ ) |
16 |
2 15
|
mpan2 |
⊢ ( 𝑟 = ( le ‘ 𝐾 ) → 𝑟 = ≤ ) |
17 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑥 ↔ 𝑥 ≤ 𝑥 ) ) |
18 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑦 ↔ 𝑥 ≤ 𝑦 ) ) |
19 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑧 ↔ 𝑦 ≤ 𝑧 ) ) |
20 |
18 19
|
anbi12d |
⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) ) |
21 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑧 ↔ 𝑥 ≤ 𝑧 ) ) |
22 |
20 21
|
imbi12d |
⊢ ( 𝑟 = ≤ → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) |
23 |
17 22
|
anbi12d |
⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
24 |
23
|
ralbidv |
⊢ ( 𝑟 = ≤ → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
25 |
24
|
2ralbidv |
⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
26 |
16 25
|
syl |
⊢ ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
27 |
14 26
|
sylan9bb |
⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝑟 = ( le ‘ 𝐾 ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
28 |
7 8 27
|
sbc2ie |
⊢ ( [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) |
29 |
6 28
|
bitrdi |
⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |
30 |
|
df-proset |
⊢ Proset = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) } |
31 |
29 30
|
elab4g |
⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) |