ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1oiso Structured version   GIF version

Theorem f1oiso 5390
Description: Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
Assertion
Ref Expression
f1oiso ((𝐻:A1-1-ontoB 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → 𝐻 Isom 𝑅, 𝑆 (A, B))
Distinct variable groups:   x,y,z,w,A   x,B,y   x,𝐻,y,z,w   x,𝑅,y,z,w
Allowed substitution hints:   B(z,w)   𝑆(x,y,z,w)

Proof of Theorem f1oiso
Dummy variables v u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 102 . 2 ((𝐻:A1-1-ontoB 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → 𝐻:A1-1-ontoB)
2 f1of1 5050 . . 3 (𝐻:A1-1-ontoB𝐻:A1-1B)
3 df-br 3739 . . . . 5 ((𝐻v)𝑆(𝐻u) ↔ ⟨(𝐻v), (𝐻u)⟩ 𝑆)
4 eleq2 2083 . . . . . . 7 (𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)} → (⟨(𝐻v), (𝐻u)⟩ 𝑆 ↔ ⟨(𝐻v), (𝐻u)⟩ {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}))
5 f1fn 5018 . . . . . . . . 9 (𝐻:A1-1B𝐻 Fn A)
6 funfvex 5117 . . . . . . . . . . . 12 ((Fun 𝐻 v dom 𝐻) → (𝐻v) V)
76funfni 4925 . . . . . . . . . . 11 ((𝐻 Fn A v A) → (𝐻v) V)
8 funfvex 5117 . . . . . . . . . . . 12 ((Fun 𝐻 u dom 𝐻) → (𝐻u) V)
98funfni 4925 . . . . . . . . . . 11 ((𝐻 Fn A u A) → (𝐻u) V)
107, 9anim12dan 519 . . . . . . . . . 10 ((𝐻 Fn A (v A u A)) → ((𝐻v) V (𝐻u) V))
11 eqeq1 2028 . . . . . . . . . . . . . 14 (z = (𝐻v) → (z = (𝐻x) ↔ (𝐻v) = (𝐻x)))
1211anbi1d 441 . . . . . . . . . . . . 13 (z = (𝐻v) → ((z = (𝐻x) w = (𝐻y)) ↔ ((𝐻v) = (𝐻x) w = (𝐻y))))
1312anbi1d 441 . . . . . . . . . . . 12 (z = (𝐻v) → (((z = (𝐻x) w = (𝐻y)) x𝑅y) ↔ (((𝐻v) = (𝐻x) w = (𝐻y)) x𝑅y)))
14132rexbidv 2327 . . . . . . . . . . 11 (z = (𝐻v) → (x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y) ↔ x A y A (((𝐻v) = (𝐻x) w = (𝐻y)) x𝑅y)))
15 eqeq1 2028 . . . . . . . . . . . . . 14 (w = (𝐻u) → (w = (𝐻y) ↔ (𝐻u) = (𝐻y)))
1615anbi2d 440 . . . . . . . . . . . . 13 (w = (𝐻u) → (((𝐻v) = (𝐻x) w = (𝐻y)) ↔ ((𝐻v) = (𝐻x) (𝐻u) = (𝐻y))))
1716anbi1d 441 . . . . . . . . . . . 12 (w = (𝐻u) → ((((𝐻v) = (𝐻x) w = (𝐻y)) x𝑅y) ↔ (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y)))
18172rexbidv 2327 . . . . . . . . . . 11 (w = (𝐻u) → (x A y A (((𝐻v) = (𝐻x) w = (𝐻y)) x𝑅y) ↔ x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y)))
1914, 18opelopabg 3979 . . . . . . . . . 10 (((𝐻v) V (𝐻u) V) → (⟨(𝐻v), (𝐻u)⟩ {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)} ↔ x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y)))
2010, 19syl 14 . . . . . . . . 9 ((𝐻 Fn A (v A u A)) → (⟨(𝐻v), (𝐻u)⟩ {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)} ↔ x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y)))
215, 20sylan 267 . . . . . . . 8 ((𝐻:A1-1B (v A u A)) → (⟨(𝐻v), (𝐻u)⟩ {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)} ↔ x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y)))
22 anass 383 . . . . . . . . . . . . . . 15 ((((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ ((𝐻v) = (𝐻x) ((𝐻u) = (𝐻y) x𝑅y)))
23 f1fveq 5336 . . . . . . . . . . . . . . . . . 18 ((𝐻:A1-1B (v A x A)) → ((𝐻v) = (𝐻x) ↔ v = x))
24 equcom 1575 . . . . . . . . . . . . . . . . . 18 (v = xx = v)
2523, 24syl6bb 185 . . . . . . . . . . . . . . . . 17 ((𝐻:A1-1B (v A x A)) → ((𝐻v) = (𝐻x) ↔ x = v))
2625anassrs 382 . . . . . . . . . . . . . . . 16 (((𝐻:A1-1B v A) x A) → ((𝐻v) = (𝐻x) ↔ x = v))
2726anbi1d 441 . . . . . . . . . . . . . . 15 (((𝐻:A1-1B v A) x A) → (((𝐻v) = (𝐻x) ((𝐻u) = (𝐻y) x𝑅y)) ↔ (x = v ((𝐻u) = (𝐻y) x𝑅y))))
2822, 27syl5bb 181 . . . . . . . . . . . . . 14 (((𝐻:A1-1B v A) x A) → ((((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ (x = v ((𝐻u) = (𝐻y) x𝑅y))))
2928rexbidv 2305 . . . . . . . . . . . . 13 (((𝐻:A1-1B v A) x A) → (y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ y A (x = v ((𝐻u) = (𝐻y) x𝑅y))))
30 r19.42v 2445 . . . . . . . . . . . . 13 (y A (x = v ((𝐻u) = (𝐻y) x𝑅y)) ↔ (x = v y A ((𝐻u) = (𝐻y) x𝑅y)))
3129, 30syl6bb 185 . . . . . . . . . . . 12 (((𝐻:A1-1B v A) x A) → (y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ (x = v y A ((𝐻u) = (𝐻y) x𝑅y))))
3231rexbidva 2301 . . . . . . . . . . 11 ((𝐻:A1-1B v A) → (x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ x A (x = v y A ((𝐻u) = (𝐻y) x𝑅y))))
33 breq1 3741 . . . . . . . . . . . . . . 15 (x = v → (x𝑅yv𝑅y))
3433anbi2d 440 . . . . . . . . . . . . . 14 (x = v → (((𝐻u) = (𝐻y) x𝑅y) ↔ ((𝐻u) = (𝐻y) v𝑅y)))
3534rexbidv 2305 . . . . . . . . . . . . 13 (x = v → (y A ((𝐻u) = (𝐻y) x𝑅y) ↔ y A ((𝐻u) = (𝐻y) v𝑅y)))
3635ceqsrexv 2651 . . . . . . . . . . . 12 (v A → (x A (x = v y A ((𝐻u) = (𝐻y) x𝑅y)) ↔ y A ((𝐻u) = (𝐻y) v𝑅y)))
3736adantl 262 . . . . . . . . . . 11 ((𝐻:A1-1B v A) → (x A (x = v y A ((𝐻u) = (𝐻y) x𝑅y)) ↔ y A ((𝐻u) = (𝐻y) v𝑅y)))
3832, 37bitrd 177 . . . . . . . . . 10 ((𝐻:A1-1B v A) → (x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ y A ((𝐻u) = (𝐻y) v𝑅y)))
39 f1fveq 5336 . . . . . . . . . . . . . . 15 ((𝐻:A1-1B (u A y A)) → ((𝐻u) = (𝐻y) ↔ u = y))
40 equcom 1575 . . . . . . . . . . . . . . 15 (u = yy = u)
4139, 40syl6bb 185 . . . . . . . . . . . . . 14 ((𝐻:A1-1B (u A y A)) → ((𝐻u) = (𝐻y) ↔ y = u))
4241anassrs 382 . . . . . . . . . . . . 13 (((𝐻:A1-1B u A) y A) → ((𝐻u) = (𝐻y) ↔ y = u))
4342anbi1d 441 . . . . . . . . . . . 12 (((𝐻:A1-1B u A) y A) → (((𝐻u) = (𝐻y) v𝑅y) ↔ (y = u v𝑅y)))
4443rexbidva 2301 . . . . . . . . . . 11 ((𝐻:A1-1B u A) → (y A ((𝐻u) = (𝐻y) v𝑅y) ↔ y A (y = u v𝑅y)))
45 breq2 3742 . . . . . . . . . . . . 13 (y = u → (v𝑅yv𝑅u))
4645ceqsrexv 2651 . . . . . . . . . . . 12 (u A → (y A (y = u v𝑅y) ↔ v𝑅u))
4746adantl 262 . . . . . . . . . . 11 ((𝐻:A1-1B u A) → (y A (y = u v𝑅y) ↔ v𝑅u))
4844, 47bitrd 177 . . . . . . . . . 10 ((𝐻:A1-1B u A) → (y A ((𝐻u) = (𝐻y) v𝑅y) ↔ v𝑅u))
4938, 48sylan9bb 438 . . . . . . . . 9 (((𝐻:A1-1B v A) (𝐻:A1-1B u A)) → (x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ v𝑅u))
5049anandis 513 . . . . . . . 8 ((𝐻:A1-1B (v A u A)) → (x A y A (((𝐻v) = (𝐻x) (𝐻u) = (𝐻y)) x𝑅y) ↔ v𝑅u))
5121, 50bitrd 177 . . . . . . 7 ((𝐻:A1-1B (v A u A)) → (⟨(𝐻v), (𝐻u)⟩ {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)} ↔ v𝑅u))
524, 51sylan9bbr 439 . . . . . 6 (((𝐻:A1-1B (v A u A)) 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → (⟨(𝐻v), (𝐻u)⟩ 𝑆v𝑅u))
5352an32s 490 . . . . 5 (((𝐻:A1-1B 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) (v A u A)) → (⟨(𝐻v), (𝐻u)⟩ 𝑆v𝑅u))
543, 53syl5rbb 182 . . . 4 (((𝐻:A1-1B 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) (v A u A)) → (v𝑅u ↔ (𝐻v)𝑆(𝐻u)))
5554ralrimivva 2379 . . 3 ((𝐻:A1-1B 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → v A u A (v𝑅u ↔ (𝐻v)𝑆(𝐻u)))
562, 55sylan 267 . 2 ((𝐻:A1-1-ontoB 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → v A u A (v𝑅u ↔ (𝐻v)𝑆(𝐻u)))
57 df-isom 4838 . 2 (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ (𝐻:A1-1-ontoB v A u A (v𝑅u ↔ (𝐻v)𝑆(𝐻u))))
581, 56, 57sylanbrc 396 1 ((𝐻:A1-1-ontoB 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → 𝐻 Isom 𝑅, 𝑆 (A, B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1228   wcel 1374  wral 2284  wrex 2285  Vcvv 2535  cop 3353   class class class wbr 3738  {copab 3791   Fn wfn 4824  1-1wf1 4826  1-1-ontowf1o 4828  cfv 4829   Isom wiso 4830
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-v 2537  df-sbc 2742  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-opab 3793  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-f1o 4836  df-fv 4837  df-isom 4838
This theorem is referenced by:  f1oiso2  5391
  Copyright terms: Public domain W3C validator