Step | Hyp | Ref
| Expression |
1 | | phtpcrel 22600 |
. 2
⊢ Rel (
≃ph‘𝐽) |
2 | | isphtpc 22601 |
. . . 4
⊢ (𝑥(
≃ph‘𝐽)𝑦 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑦 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅)) |
3 | 2 | simp2bi 1070 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑦 ∈ (II Cn 𝐽)) |
4 | 2 | simp1bi 1069 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑥 ∈ (II Cn 𝐽)) |
5 | 2 | simp3bi 1071 |
. . . . 5
⊢ (𝑥(
≃ph‘𝐽)𝑦 → (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅) |
6 | | n0 3890 |
. . . . 5
⊢ ((𝑥(PHtpy‘𝐽)𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
7 | 5, 6 | sylib 207 |
. . . 4
⊢ (𝑥(
≃ph‘𝐽)𝑦 → ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
8 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑥 ∈ (II Cn 𝐽)) |
9 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑦 ∈ (II Cn 𝐽)) |
10 | | eqid 2610 |
. . . . . 6
⊢ (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) |
11 | | simpr 476 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
12 | 8, 9, 10, 11 | phtpycom 22595 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) ∈ (𝑦(PHtpy‘𝐽)𝑥)) |
13 | | ne0i 3880 |
. . . . 5
⊢ ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝑓(1 − 𝑣))) ∈ (𝑦(PHtpy‘𝐽)𝑥) → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
15 | 7, 14 | exlimddv 1850 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑦 → (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅) |
16 | | isphtpc 22601 |
. . 3
⊢ (𝑦(
≃ph‘𝐽)𝑥 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑥) ≠ ∅)) |
17 | 3, 4, 15, 16 | syl3anbrc 1239 |
. 2
⊢ (𝑥(
≃ph‘𝐽)𝑦 → 𝑦( ≃ph‘𝐽)𝑥) |
18 | 4 | adantr 480 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑥 ∈ (II Cn 𝐽)) |
19 | | simpr 476 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑦( ≃ph‘𝐽)𝑧) |
20 | | isphtpc 22601 |
. . . . 5
⊢ (𝑦(
≃ph‘𝐽)𝑧 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅)) |
21 | 19, 20 | sylib 207 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑦 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅)) |
22 | 21 | simp2d 1067 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑧 ∈ (II Cn 𝐽)) |
23 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑥(PHtpy‘𝐽)𝑦) ≠ ∅) |
24 | 23, 6 | sylib 207 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
25 | 21 | simp3d 1068 |
. . . . . 6
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑦(PHtpy‘𝐽)𝑧) ≠ ∅) |
26 | | n0 3890 |
. . . . . 6
⊢ ((𝑦(PHtpy‘𝐽)𝑧) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
27 | 25, 26 | sylib 207 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
28 | | eeanv 2170 |
. . . . 5
⊢
(∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) ↔ (∃𝑓 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ ∃𝑔 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) |
29 | 24, 27, 28 | sylanbrc 695 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) |
30 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) |
31 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑥 ∈ (II Cn 𝐽)) |
32 | 21 | simp1d 1066 |
. . . . . . . . 9
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑦 ∈ (II Cn 𝐽)) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑦 ∈ (II Cn 𝐽)) |
34 | 22 | adantr 480 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑧 ∈ (II Cn 𝐽)) |
35 | | simprl 790 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦)) |
36 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) |
37 | 30, 31, 33, 34, 35, 36 | phtpycc 22598 |
. . . . . . 7
⊢ (((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) ∧ (𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧))) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ if(𝑣 ≤ (1 / 2), (𝑢𝑓(2 · 𝑣)), (𝑢𝑔((2 · 𝑣) − 1)))) ∈ (𝑥(PHtpy‘𝐽)𝑧)) |
38 | | ne0i 3880 |
. . . . . . 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 449 |
. . . . 5
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → ((𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
41 | 40 | exlimdvv 1849 |
. . . 4
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (∃𝑓∃𝑔(𝑓 ∈ (𝑥(PHtpy‘𝐽)𝑦) ∧ 𝑔 ∈ (𝑦(PHtpy‘𝐽)𝑧)) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
42 | 29, 41 | mpd 15 |
. . 3
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅) |
43 | | isphtpc 22601 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑧 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑧 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑧) ≠ ∅)) |
44 | 18, 22, 42, 43 | syl3anbrc 1239 |
. 2
⊢ ((𝑥(
≃ph‘𝐽)𝑦 ∧ 𝑦( ≃ph‘𝐽)𝑧) → 𝑥( ≃ph‘𝐽)𝑧) |
45 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) = (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) |
46 | | id 22 |
. . . . . . . 8
⊢ (𝑥 ∈ (II Cn 𝐽) → 𝑥 ∈ (II Cn 𝐽)) |
47 | 45, 46 | phtpyid 22596 |
. . . . . . 7
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) ∈ (𝑥(PHtpy‘𝐽)𝑥)) |
48 | | ne0i 3880 |
. . . . . . 7
⊢ ((𝑦 ∈ (0[,]1), 𝑧 ∈ (0[,]1) ↦ (𝑥‘𝑦)) ∈ (𝑥(PHtpy‘𝐽)𝑥) → (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) |
49 | 47, 48 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) |
50 | 49 | ancli 572 |
. . . . 5
⊢ (𝑥 ∈ (II Cn 𝐽) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
51 | 50 | pm4.71ri 663 |
. . . 4
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) ∧ 𝑥 ∈ (II Cn 𝐽))) |
52 | | df-3an 1033 |
. . . 4
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅ ∧ 𝑥 ∈ (II Cn 𝐽)) ↔ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅) ∧ 𝑥 ∈ (II Cn 𝐽))) |
53 | | 3ancomb 1040 |
. . . 4
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅ ∧ 𝑥 ∈ (II Cn 𝐽)) ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
54 | 51, 52, 53 | 3bitr2i 287 |
. . 3
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
55 | | isphtpc 22601 |
. . 3
⊢ (𝑥(
≃ph‘𝐽)𝑥 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ 𝑥 ∈ (II Cn 𝐽) ∧ (𝑥(PHtpy‘𝐽)𝑥) ≠ ∅)) |
56 | 54, 55 | bitr4i 266 |
. 2
⊢ (𝑥 ∈ (II Cn 𝐽) ↔ 𝑥( ≃ph‘𝐽)𝑥) |
57 | 1, 17, 44, 56 | iseri 7656 |
1
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |