Theorem isorel 5944

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 5333	. . 3 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simprbi 275	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
3		breq1 4089	. . . 4 ⊢ (𝑥 = 𝐶 → (𝑥𝑅𝑦 ↔ 𝐶𝑅𝑦))
4		fveq2 5635	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐻‘𝑥) = (𝐻‘𝐶))
5	4	breq1d 4096	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)))
6	3, 5	bibi12d 235	. . 3 ⊢ (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦))))
7		breq2 4090	. . . 4 ⊢ (𝑦 = 𝐷 → (𝐶𝑅𝑦 ↔ 𝐶𝑅𝐷))
8		fveq2 5635	. . . . 5 ⊢ (𝑦 = 𝐷 → (𝐻‘𝑦) = (𝐻‘𝐷))
9	8	breq2d 4098	. . . 4 ⊢ (𝑦 = 𝐷 → ((𝐻‘𝐶)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))
10	7, 9	bibi12d 235	. . 3 ⊢ (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))))
11	6, 10	rspc2v 2921	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))))
12	2, 11	mpan9 281	1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508   class class class wbr 4086  –1-1-onto→wf1o 5323  ‘cfv 5324   Isom wiso 5325

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-isom 5333

This theorem is referenced by:  isoresbr  5945  isoini  5954  isopolem  5958  isosolem  5960  smoiso  6463  isotilem  7199  supisolem  7201  ordiso2  7228  leisorel  11094  zfz1isolemiso  11096  seq3coll  11099