Theorem isoini2 5458

Description: Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)

Hypotheses

Ref	Expression
isoini2.1	⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))
isoini2.2	⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))

Assertion

Ref	Expression
isoini2	⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))

Proof of Theorem isoini2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isof1o 5447	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
2		f1of1 5125	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–1-1→𝐵)
3	1, 2	syl 14	. . . . 5 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1→𝐵)
4	3	adantr 261	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → 𝐻:𝐴–1-1→𝐵)
5		isoini2.1	. . . . 5 ⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))
6		inss1 3157	. . . . 5 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴
7	5, 6	eqsstri 2975	. . . 4 ⊢ 𝐶 ⊆ 𝐴
8		f1ores 5141	. . . 4 ⊢ ((𝐻:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
9	4, 7, 8	sylancl 392	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
10		isoini 5457	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})))
11	5	imaeq2i 4666	. . . . 5 ⊢ (𝐻 “ 𝐶) = (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋})))
12		isoini2.2	. . . . 5 ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))
13	10, 11, 12	3eqtr4g 2097	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ 𝐶) = 𝐷)
14		f1oeq3 5119	. . . 4 ⊢ ((𝐻 “ 𝐶) = 𝐷 → ((𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶) ↔ (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷))
15	13, 14	syl 14	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ((𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶) ↔ (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷))
16	9, 15	mpbid 135	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷)
17		df-isom 4911	. . . . . . 7 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
18	17	simprbi 260	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
19	18	adantr 261	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20		ssralv 3004	. . . . . 6 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
21	20	ralimdv 2388	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
22	7, 19, 21	mpsyl 59	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
23		ssralv 3004	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
24	7, 22, 23	mpsyl 59	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
25		fvres 5198	. . . . . . 7 ⊢ (𝑥 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑥) = (𝐻‘𝑥))
26		fvres 5198	. . . . . . 7 ⊢ (𝑦 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑦) = (𝐻‘𝑦))
27	25, 26	breqan12d 3779	. . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦) ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
28	27	bibi2d 221	. . . . 5 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → ((𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
29	28	ralbidva 2322	. . . 4 ⊢ (𝑥 ∈ 𝐶 → (∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
30	29	ralbiia 2338	. . 3 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
31	24, 30	sylibr 137	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)))
32		df-isom 4911	. 2 ⊢ ((𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷) ↔ ((𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦))))
33	16, 31, 32	sylanbrc 394	1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ∀wral 2306   ∩ cin 2916   ⊆ wss 2917  {csn 3375   class class class wbr 3764  ^◡ccnv 4344   ↾ cres 4347   “ cima 4348  –1-1→wf1 4899  –1-1-onto→wf1o 4901  ‘cfv 4902   Isom wiso 4903

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-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-sbc 2765  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-mpt 3820  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-isom 4911

This theorem is referenced by: (None)