Step | Hyp | Ref
| Expression |
1 | | phtpcrel 22792 |
. 2
⊢ Rel (
≃ph‘𝐽) |
2 | | isphtpc 22793 |
. . . 4
⊢ (𝑥(
≃ph‘𝐽)𝑦 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅)) |
3 | 2 | simp2bi 1077 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑦 ∈ (II Cn 𝐽)) |
4 | 2 | simp1bi 1076 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑥 ∈ (II Cn 𝐽)) |
5 | 2 | simp3bi 1078 |
. . . . 5
⊢ (𝑥(
≃ph‘𝐽)𝑦 → (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅) |
6 | | n0 3931 |
. . . . 5
⊢ ((𝑥(PHtpy‘𝐽)𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
7 | 5, 6 | sylib 208 |
. . . 4
⊢ (𝑥(
≃ph‘𝐽)𝑦 → ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
8 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑥 ∈ (II Cn 𝐽)) |
9 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑦 ∈ (II Cn 𝐽)) |
10 | | eqid 2622 |
. . . . . 6
⊢ (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) |
11 | | simpr 477 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
12 | 8, 9, 10, 11 | phtpycom 22787 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) ∈ (𝑦(PHtpy‘𝐽)𝑥)) |
13 | | ne0i 3921 |
. . . . 5
⊢ ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) ∈ (𝑦(PHtpy‘𝐽)𝑥) → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
15 | 7, 14 | exlimddv 1863 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
16 | | isphtpc 22793 |
. . 3
⊢ (𝑦(
≃ph‘𝐽)𝑥 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅)) |
17 | 3, 4, 15, 16 | syl3anbrc 1246 |
. 2
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑦( ≃ph‘𝐽)𝑥) |
18 | 4 | adantr 481 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑥 ∈ (II Cn 𝐽)) |
19 | | simpr 477 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑦( ≃ph‘𝐽)𝑧) |
20 | | isphtpc 22793 |
. . . . 5
⊢ (𝑦(
≃ph‘𝐽)𝑧 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅)) |
21 | 19, 20 | sylib 208 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑦 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅)) |
22 | 21 | simp2d 1074 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑧 ∈ (II Cn 𝐽)) |
23 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅) |
24 | 23, 6 | sylib 208 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
25 | 21 | simp3d 1075 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅) |
26 | | n0 3931 |
. . . . . 6
⊢ ((𝑦(PHtpy‘𝐽)𝑧) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
27 | 25, 26 | sylib 208 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
28 | | eeanv 2182 |
. . . . 5
⊢
(∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) ↔ (∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) |
29 | 24, 27, 28 | sylanbrc 698 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) |
30 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) |
31 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑥 ∈ (II Cn 𝐽)) |
32 | 21 | simp1d 1073 |
. . . . . . . . 9
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑦 ∈ (II Cn 𝐽)) |
33 | 32 | adantr 481 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑦 ∈ (II Cn 𝐽)) |
34 | 22 | adantr 481 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑧 ∈ (II Cn 𝐽)) |
35 | | simprl 794 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
36 | | simprr 796 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
37 | 30, 31, 33, 34, 35, 36 | phtpycc 22790 |
. . . . . . 7
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) ∈ (𝑥(PHtpy‘𝐽)𝑧)) |
38 | | ne0i 3921 |
. . . . . . 7
⊢ ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) ∈ (𝑥(PHtpy‘𝐽)𝑧) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅) |
40 | 39 | ex 450 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ((𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
41 | 40 | exlimdvv 1862 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
42 | 29, 41 | mpd 15 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅) |
43 | | isphtpc 22793 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑧 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
44 | 18, 22, 42, 43 | syl3anbrc 1246 |
. 2
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑥( ≃ph‘𝐽)𝑧) |
45 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) = (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) |
46 | | id 22 |
. . . . . . . 8
⊢ (𝑥 ∈ (II Cn 𝐽) → 𝑥 ∈ (II Cn 𝐽)) |
47 | 45, 46 | phtpyid 22788 |
. . . . . . 7
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) ∈ (𝑥(PHtpy‘𝐽)𝑥)) |
48 | | ne0i 3921 |
. . . . . . 7
⊢ ((𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) ∈ (𝑥(PHtpy‘𝐽)𝑥) → (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) |
49 | 47, 48 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) |
50 | 49 | ancli 574 |
. . . . 5
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
51 | 50 | pm4.71ri 665 |
. . . 4
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) ∧ 𝑥 ∈ (II Cn 𝐽))) |
52 | | df-3an 1039 |
. . . 4
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅ ∧ 𝑥 ∈ (II Cn 𝐽)) ↔ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) ∧ 𝑥 ∈ (II Cn 𝐽))) |
53 | | 3ancomb 1047 |
. . . 4
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅ ∧ 𝑥 ∈ (II Cn 𝐽)) ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
54 | 51, 52, 53 | 3bitr2i 288 |
. . 3
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
55 | | isphtpc 22793 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑥 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
56 | 54, 55 | bitr4i 267 |
. 2
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ 𝑥( ≃ph‘𝐽)𝑥) |
57 | 1, 17, 44, 56 | iseri 7769 |
1
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |