Theorem isorel 7346

Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)

Assertion

Ref	Expression
isorel	⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Proof of Theorem isorel

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

Step	Hyp	Ref	Expression
1		df-isom 6570	. . 3 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simprbi 496	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
3		breq1 5146	. . . 4 ⊢ (𝑥 = 𝐶 → (𝑥𝑅𝑦 ↔ 𝐶𝑅𝑦))
4		fveq2 6906	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐻‘𝑥) = (𝐻‘𝐶))
5	4	breq1d 5153	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)))
6	3, 5	bibi12d 345	. . 3 ⊢ (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦))))
7		breq2 5147	. . . 4 ⊢ (𝑦 = 𝐷 → (𝐶𝑅𝑦 ↔ 𝐶𝑅𝐷))
8		fveq2 6906	. . . . 5 ⊢ (𝑦 = 𝐷 → (𝐻‘𝑦) = (𝐻‘𝐷))
9	8	breq2d 5155	. . . 4 ⊢ (𝑦 = 𝐷 → ((𝐻‘𝐶)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
10	7, 9	bibi12d 345	. . 3 ⊢ (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))))
11	6, 10	rspc2v 3633	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))))
12	2, 11	mpan9 506	1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061   class class class wbr 5143  –1-1-onto→wf1o 6560  ‘cfv 6561   Isom wiso 6562

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-isom 6570

This theorem is referenced by:  soisores  7347  isomin  7357  isoini  7358  isopolem  7365  isosolem  7367  weniso  7374  smoiso  8402  supisolem  9513  ordiso2  9555  cantnflt  9712  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  wemapwe  9737  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  leisorel  14499  seqcoll  14503  seqcoll2  14504  isercoll  15704  ordthmeolem  23809  iccpnfhmeo  24976  xrhmeo  24977  dvcnvrelem1  26056  dvcvx  26059  isoun  32711  erdszelem8  35203  erdsze2lem2  35209  cantnfresb  43337  fourierdlem20  46142  fourierdlem46  46167  fourierdlem50  46171  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem76  46197  fourierdlem79  46200  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235