Theorem isopolem 5382

Description: Lemma for isopo 5383. (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 5368	. . . . . . . . . . 11 ⊢ (𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻:A–1-1-onto→B)
2		f1of 5047	. . . . . . . . . . 11 ⊢ (𝐻:A–1-1-onto→B → 𝐻:A⟶B)
3		ffvelrn 5221	. . . . . . . . . . . . 13 ⊢ ((𝐻:A⟶B ∧ 𝑑 ∈ A) → (𝐻‘𝑑) ∈ B)
4	3	ex 108	. . . . . . . . . . . 12 ⊢ (𝐻:A⟶B → (𝑑 ∈ A → (𝐻‘𝑑) ∈ B))
5		ffvelrn 5221	. . . . . . . . . . . . 13 ⊢ ((𝐻:A⟶B ∧ 𝑒 ∈ A) → (𝐻‘𝑒) ∈ B)
6	5	ex 108	. . . . . . . . . . . 12 ⊢ (𝐻:A⟶B → (𝑒 ∈ A → (𝐻‘𝑒) ∈ B))
7		ffvelrn 5221	. . . . . . . . . . . . 13 ⊢ ((𝐻:A⟶B ∧ f ∈ A) → (𝐻‘f) ∈ B)
8	7	ex 108	. . . . . . . . . . . 12 ⊢ (𝐻:A⟶B → (f ∈ A → (𝐻‘f) ∈ B))
9	4, 6, 8	3anim123d 1197	. . . . . . . . . . 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 3739	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝐻‘𝑑) ∧ 𝑎 = (𝐻‘𝑑)) → (𝑎𝑆𝑎 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
13	12	anidms 379	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑎 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
14	13	notbid 579	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐻‘𝑑) → (¬ 𝑎𝑆𝑎 ↔ ¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
15		breq1 3737	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑏 ↔ (𝐻‘𝑑)𝑆𝑏))
16	15	anbi1d 441	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝐻‘𝑑) → ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐)))
17		breq1 3737	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝐻‘𝑑) → (𝑎𝑆𝑐 ↔ (𝐻‘𝑑)𝑆𝑐))
18	16, 17	imbi12d 223	. . . . . . . . . . 11 ⊢ (𝑎 = (𝐻‘𝑑) → (((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)))
19	14, 18	anbi12d 445	. . . . . . . . . 10 ⊢ (𝑎 = (𝐻‘𝑑) → ((¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐))))
20		breq2 3738	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝐻‘𝑒) → ((𝐻‘𝑑)𝑆𝑏 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒)))
21		breq1 3737	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝐻‘𝑒) → (𝑏𝑆𝑐 ↔ (𝐻‘𝑒)𝑆𝑐))
22	20, 21	anbi12d 445	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝐻‘𝑒) → (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐)))
23	22	imbi1d 220	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐻‘𝑒) → ((((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)))
24	23	anbi2d 440	. . . . . . . . . 10 ⊢ (𝑏 = (𝐻‘𝑒) → ((¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆𝑏 ∧ 𝑏𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐))))
25		breq2 3738	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝐻‘f) → ((𝐻‘𝑒)𝑆𝑐 ↔ (𝐻‘𝑒)𝑆(𝐻‘f)))
26	25	anbi2d 440	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝐻‘f) → (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) ↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f))))
27		breq2 3738	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝐻‘f) → ((𝐻‘𝑑)𝑆𝑐 ↔ (𝐻‘𝑑)𝑆(𝐻‘f)))
28	26, 27	imbi12d 223	. . . . . . . . . . 11 ⊢ (𝑐 = (𝐻‘f) → ((((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐) ↔ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f))))
29	28	anbi2d 440	. . . . . . . . . 10 ⊢ (𝑐 = (𝐻‘f) → ((¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆𝑐) → (𝐻‘𝑑)𝑆𝑐)) ↔ (¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑) ∧ (((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f)) → (𝐻‘𝑑)𝑆(𝐻‘f)))))
30	19, 24, 29	rspc3v 2638	. . . . . . . . 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 896	. . . . . . . . . . 11 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → 𝑑 ∈ A)
34		isorel 5369	. . . . . . . . . . 11 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑑 ∈ A)) → (𝑑𝑅𝑑 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
35	32, 33, 33, 34	syl12anc 1117	. . . . . . . . . 10 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → (𝑑𝑅𝑑 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
36	35	notbid 579	. . . . . . . . 9 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → (¬ 𝑑𝑅𝑑 ↔ ¬ (𝐻‘𝑑)𝑆(𝐻‘𝑑)))
37		simpr2 897	. . . . . . . . . . . 12 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → 𝑒 ∈ A)
38		isorel 5369	. . . . . . . . . . . 12 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A)) → (𝑑𝑅𝑒 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒)))
39	32, 33, 37, 38	syl12anc 1117	. . . . . . . . . . 11 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → (𝑑𝑅𝑒 ↔ (𝐻‘𝑑)𝑆(𝐻‘𝑒)))
40		simpr3 898	. . . . . . . . . . . 12 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → f ∈ A)
41		isorel 5369	. . . . . . . . . . . 12 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑒 ∈ A ∧ f ∈ A)) → (𝑒𝑅f ↔ (𝐻‘𝑒)𝑆(𝐻‘f)))
42	32, 37, 40, 41	syl12anc 1117	. . . . . . . . . . 11 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → (𝑒𝑅f ↔ (𝐻‘𝑒)𝑆(𝐻‘f)))
43	39, 42	anbi12d 445	. . . . . . . . . 10 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ 𝑒 ∈ A ∧ f ∈ A)) → ((𝑑𝑅𝑒 ∧ 𝑒𝑅f) ↔ ((𝐻‘𝑑)𝑆(𝐻‘𝑒) ∧ (𝐻‘𝑒)𝑆(𝐻‘f))))
44		isorel 5369	. . . . . . . . . . 11 ⊢ ((𝐻 Isom 𝑅, 𝑆 (A, B) ∧ (𝑑 ∈ A ∧ f ∈ A)) → (𝑑𝑅f ↔ (𝐻‘𝑑)𝑆(𝐻‘f)))
45	32, 33, 40, 44	syl12anc 1117	. . . . . . . . . 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 445	. . . . . . . 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 2376	. . 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 4003	. 2 ⊢ (𝑆 Po B ↔ ∀𝑎 ∈ B ∀𝑏 ∈ B ∀𝑐 ∈ B (¬ 𝑎𝑆𝑎 ∧ ((𝑎𝑆𝑏 ∧ 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
55		df-po 4003	. 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 871   = wceq 1226   ∈ wcel 1370  ∀wral 2280   class class class wbr 3734   Po wpo 4001  ⟶wf 4821  –1-1-onto→wf1o 4824  ‘cfv 4825   Isom wiso 4826

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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-po 4003  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-f1o 4832  df-fv 4833  df-isom 4834

This theorem is referenced by:  isopo  5383  isosolem  5384