Theorem isoini2 5814

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 5802	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)
2		f1of1 5456	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻:𝐴–1-1→𝐵)
3	1, 2	syl 14	. . . . 5 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1→𝐵)
4	3	adantr 276	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → 𝐻:𝐴–1-1→𝐵)
5		isoini2.1	. . . . 5 ⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋}))
6		inss1 3355	. . . . 5 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴
7	5, 6	eqsstri 3187	. . . 4 ⊢ 𝐶 ⊆ 𝐴
8		f1ores 5472	. . . 4 ⊢ ((𝐻:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
9	4, 7, 8	sylancl 413	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶))
10		isoini 5813	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})))
11	5	imaeq2i 4964	. . . . 5 ⊢ (𝐻 “ 𝐶) = (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝑋})))
12		isoini2.2	. . . . 5 ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)}))
13	10, 11, 12	3eqtr4g 2235	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 “ 𝐶) = 𝐷)
14		f1oeq3 5447	. . . 4 ⊢ ((𝐻 “ 𝐶) = 𝐷 → ((𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶) ↔ (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷))
15	13, 14	syl 14	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ((𝐻 ↾ 𝐶):𝐶–1-1-onto→(𝐻 “ 𝐶) ↔ (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷))
16	9, 15	mpbid 147	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷)
17		df-isom 5221	. . . . . . 7 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
18	17	simprbi 275	. . . . . 6 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
19	18	adantr 276	. . . . 5 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20		ssralv 3219	. . . . . 6 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
21	20	ralimdv 2545	. . . . 5 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
22	7, 19, 21	mpsyl 65	. . . 4 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
23		ssralv 3219	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
24	7, 22, 23	mpsyl 65	. . 3 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
25		fvres 5535	. . . . . . 7 ⊢ (𝑥 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑥) = (𝐻‘𝑥))
26		fvres 5535	. . . . . . 7 ⊢ (𝑦 ∈ 𝐶 → ((𝐻 ↾ 𝐶)‘𝑦) = (𝐻‘𝑦))
27	25, 26	breqan12d 4016	. . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦) ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
28	27	bibi2d 232	. . . . 5 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → ((𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
29	28	ralbidva 2473	. . . 4 ⊢ (𝑥 ∈ 𝐶 → (∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
30	29	ralbiia 2491	. . 3 ⊢ (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
31	24, 30	sylibr 134	. 2 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦)))
32		df-isom 5221	. 2 ⊢ ((𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷) ↔ ((𝐻 ↾ 𝐶):𝐶–1-1-onto→𝐷 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ ((𝐻 ↾ 𝐶)‘𝑥)𝑆((𝐻 ↾ 𝐶)‘𝑦))))
33	16, 31, 32	sylanbrc 417	1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ∀wral 2455   ∩ cin 3128   ⊆ wss 3129  {csn 3591   class class class wbr 4000  ^◡ccnv 4622   ↾ cres 4625   “ cima 4626  –1-1→wf1 5209  –1-1-onto→wf1o 5211  ‘cfv 5212   Isom wiso 5213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221

This theorem is referenced by: (None)