Theorem isopolem 5404

Description: Lemma for isopo 5405. (Contributed by Stefan O'Rear, 16-Nov-2014.)

Assertion

Ref	Expression
isopolem	⊢ (𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑆 Po B → 𝑅 Po A))

Proof of Theorem isopolem

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f are mutually distinct and distinct from all other variables.

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))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300   class class class wbr 3755   Po wpo 4022  ⟶wf 4841  –1-1-onto→wf1o 4844  ‘cfv 4845   Isom wiso 4846

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-po 4024  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-f1o 4852  df-fv 4853  df-isom 4854

This theorem is referenced by:  isopo  5405  isosolem  5406