Theorem isoini2 7314

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 7298	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
2		f1of1 6799	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–1-1→𝐵)
3	1, 2	syl 17	. . . . 5 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1→𝐵)
4	3	adantr 480	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → 𝐻:𝐴–1-1→𝐵)
5		isoini2.1	. . . . 5 ⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))
6		inss1 4200	. . . . 5 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴
7	5, 6	eqsstri 3993	. . . 4 ⊢ 𝐶 ⊆ 𝐴
8		f1ores 6814	. . . 4 ⊢ ((𝐻:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
9	4, 7, 8	sylancl 586	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
10		isoini 7313	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})))
11	5	imaeq2i 6029	. . . . 5 ⊢ (𝐻 “ 𝐶) = (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋})))
12		isoini2.2	. . . . 5 ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))
13	10, 11, 12	3eqtr4g 2789	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ 𝐶) = 𝐷)
14	13	f1oeq3d 6797	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ((𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶) ↔ (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷))
15	9, 14	mpbid 232	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷)
16		df-isom 6520	. . . . . . 7 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
17	16	simprbi 496	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
18	17	adantr 480	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
19		ssralv 4015	. . . . . 6 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
20	19	ralimdv 3147	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
21	7, 18, 20	mpsyl 68	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
22		ssralv 4015	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
23	7, 21, 22	mpsyl 68	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
24		fvres 6877	. . . . . . 7 ⊢ (𝑥 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑥) = (𝐻‘𝑥))
25		fvres 6877	. . . . . . 7 ⊢ (𝑦 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑦) = (𝐻‘𝑦))
26	24, 25	breqan12d 5123	. . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦) ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
27	26	bibi2d 342	. . . . 5 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → ((𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
28	27	ralbidva 3154	. . . 4 ⊢ (𝑥 ∈ 𝐶 → (∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
29	28	ralbiia 3073	. . 3 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
30	23, 29	sylibr 234	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)))
31		df-isom 6520	. 2 ⊢ ((𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷) ↔ ((𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦))))
32	15, 30, 31	sylanbrc 583	1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ∩ cin 3913   ⊆ wss 3914  {csn 4589   class class class wbr 5107  ^◡ccnv 5637   ↾ cres 5640   “ cima 5641  –1-1→wf1 6508  –1-1-onto→wf1o 6510  ‘cfv 6511   Isom wiso 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520

This theorem is referenced by:  fz1isolem  14426