Step | Hyp | Ref
| Expression |
1 | | isof1o 5390 |
. . . . . . . . . . 11
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → 𝐻:A–1-1-onto→B) |
2 | | f1of 5069 |
. . . . . . . . . . 11
⊢ (𝐻:A–1-1-onto→B →
𝐻:A⟶B) |
3 | | ffvelrn 5243 |
. . . . . . . . . . . . 13
⊢ ((𝐻:A⟶B ∧ 𝑑
∈ A)
→ (𝐻‘𝑑) ∈ B) |
4 | 3 | ex 108 |
. . . . . . . . . . . 12
⊢ (𝐻:A⟶B
→ (𝑑 ∈ A →
(𝐻‘𝑑) ∈
B)) |
5 | | ffvelrn 5243 |
. . . . . . . . . . . . 13
⊢ ((𝐻:A⟶B ∧ 𝑒
∈ A)
→ (𝐻‘𝑒) ∈ B) |
6 | 5 | ex 108 |
. . . . . . . . . . . 12
⊢ (𝐻:A⟶B
→ (𝑒 ∈ A →
(𝐻‘𝑒) ∈
B)) |
7 | | ffvelrn 5243 |
. . . . . . . . . . . . 13
⊢ ((𝐻:A⟶B ∧ f ∈ A) →
(𝐻‘f) ∈ B) |
8 | 7 | ex 108 |
. . . . . . . . . . . 12
⊢ (𝐻:A⟶B
→ (f ∈ A →
(𝐻‘f) ∈ B)) |
9 | 4, 6, 8 | 3anim123d 1213 |
. . . . . . . . . . 11
⊢ (𝐻:A⟶B
→ ((𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A) →
((𝐻‘𝑑) ∈
B ∧ (𝐻‘𝑒) ∈
B ∧ (𝐻‘f) ∈ B))) |
10 | 1, 2, 9 | 3syl 17 |
. . . . . . . . . 10
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → ((𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A) → ((𝐻‘𝑑) ∈
B ∧ (𝐻‘𝑒) ∈
B ∧ (𝐻‘f) ∈ B))) |
11 | 10 | imp 115 |
. . . . . . . . 9
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
((𝐻‘𝑑) ∈
B ∧ (𝐻‘𝑒) ∈
B ∧ (𝐻‘f) ∈ B)) |
12 | | breq12 3760 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝐻‘𝑑) ∧ 𝑎 = (𝐻‘𝑑)) → (𝑎𝑆𝑎 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
13 | 12 | anidms 377 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑎 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
14 | 13 | notbid 591 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝐻‘𝑑) → (¬ 𝑎𝑆𝑎 ↔ ¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
15 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑏 ↔ (𝐻‘𝑑)𝑆𝑏)) |
16 | 15 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐻‘𝑑) → ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐))) |
17 | | breq1 3758 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑐 ↔ (𝐻‘𝑑)𝑆𝑐)) |
18 | 16, 17 | imbi12d 223 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝐻‘𝑑) → (((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐))) |
19 | 14, 18 | anbi12d 442 |
. . . . . . . . . 10
⊢ (𝑎 = (𝐻‘𝑑) → ((¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)))) |
20 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝐻‘𝑒) → ((𝐻‘𝑑)𝑆𝑏 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒))) |
21 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝐻‘𝑒) → (𝑏𝑆𝑐 ↔ (𝐻‘𝑒)𝑆𝑐)) |
22 | 20, 21 | anbi12d 442 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝐻‘𝑒) → (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐))) |
23 | 22 | imbi1d 220 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝐻‘𝑒) → ((((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐))) |
24 | 23 | anbi2d 437 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐻‘𝑒) → ((¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)))) |
25 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝐻‘f) → ((𝐻‘𝑒)𝑆𝑐 ↔ (𝐻‘𝑒)𝑆(𝐻‘f))) |
26 | 25 | anbi2d 437 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐻‘f) → (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)))) |
27 | | breq2 3759 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝐻‘f) → ((𝐻‘𝑑)𝑆𝑐 ↔ (𝐻‘𝑑)𝑆(𝐻‘f))) |
28 | 26, 27 | imbi12d 223 |
. . . . . . . . . . 11
⊢ (𝑐 = (𝐻‘f) → ((((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f)))) |
29 | 28 | anbi2d 437 |
. . . . . . . . . 10
⊢ (𝑐 = (𝐻‘f) → ((¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f))))) |
30 | 19, 24, 29 | rspc3v 2659 |
. . . . . . . . 9
⊢ (((𝐻‘𝑑) ∈
B ∧ (𝐻‘𝑒) ∈
B ∧ (𝐻‘f) ∈ B) → (∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f))))) |
31 | 11, 30 | syl 14 |
. . . . . . . 8
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f))))) |
32 | | simpl 102 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
𝐻 Isom 𝑅, 𝑆 (A,
B)) |
33 | | simpr1 909 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
𝑑 ∈ A) |
34 | | isorel 5391 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑑
∈ A))
→ (𝑑𝑅𝑑 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
35 | 32, 33, 33, 34 | syl12anc 1132 |
. . . . . . . . . 10
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(𝑑𝑅𝑑 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
36 | 35 | notbid 591 |
. . . . . . . . 9
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(¬ 𝑑𝑅𝑑 ↔ ¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑))) |
37 | | simpr2 910 |
. . . . . . . . . . . 12
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
𝑒 ∈ A) |
38 | | isorel 5391 |
. . . . . . . . . . . 12
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A))
→ (𝑑𝑅𝑒 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒))) |
39 | 32, 33, 37, 38 | syl12anc 1132 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(𝑑𝑅𝑒 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒))) |
40 | | simpr3 911 |
. . . . . . . . . . . 12
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
f ∈
A) |
41 | | isorel 5391 |
. . . . . . . . . . . 12
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑒 ∈ A ∧ f ∈ A)) →
(𝑒𝑅f ↔
(𝐻‘𝑒)𝑆(𝐻‘f))) |
42 | 32, 37, 40, 41 | syl12anc 1132 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(𝑒𝑅f ↔
(𝐻‘𝑒)𝑆(𝐻‘f))) |
43 | 39, 42 | anbi12d 442 |
. . . . . . . . . 10
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)))) |
44 | | isorel 5391 |
. . . . . . . . . . 11
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ f ∈ A)) →
(𝑑𝑅f ↔
(𝐻‘𝑑)𝑆(𝐻‘f))) |
45 | 32, 33, 40, 44 | syl12anc 1132 |
. . . . . . . . . 10
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(𝑑𝑅f ↔
(𝐻‘𝑑)𝑆(𝐻‘f))) |
46 | 43, 45 | imbi12d 223 |
. . . . . . . . 9
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f)
↔ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f)))) |
47 | 36, 46 | anbi12d 442 |
. . . . . . . 8
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
((¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))
↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f))))) |
48 | 31, 47 | sylibrd 158 |
. . . . . . 7
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f)))) |
49 | 48 | ex 108 |
. . . . . 6
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → ((𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A) → (∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))))) |
50 | 49 | com23 72 |
. . . . 5
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → ((𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A) → (¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))))) |
51 | 50 | imp31 243 |
. . . 4
⊢ (((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ ∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))) ∧ (𝑑 ∈ A ∧ 𝑒
∈ A ∧ f ∈ A)) →
(¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))) |
52 | 51 | ralrimivvva 2396 |
. . 3
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ ∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))) → ∀𝑑 ∈ A ∀𝑒 ∈ A ∀f ∈ A (¬
𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))) |
53 | 52 | ex 108 |
. 2
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → ∀𝑑 ∈ A ∀𝑒 ∈ A ∀f ∈ A (¬
𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f)))) |
54 | | df-po 4024 |
. 2
⊢ (𝑆 Po B ↔ ∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬
𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐))) |
55 | | df-po 4024 |
. 2
⊢ (𝑅 Po A ↔ ∀𝑑 ∈ A ∀𝑒 ∈ A ∀f ∈ A (¬ 𝑑𝑅𝑑 ∧ ((𝑑𝑅𝑒 ∧ 𝑒𝑅f)
→ 𝑑𝑅f))) |
56 | 53, 54, 55 | 3imtr4g 194 |
1
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (𝑆 Po B
→ 𝑅 Po A)) |