MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1eqcocnvOLD Structured version   Visualization version   GIF version

Theorem f1eqcocnvOLD 7248
Description: Obsolete version of f1eqcocnv 7247 as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
f1eqcocnvOLD ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝐹 = 𝐺 ↔ (𝐹𝐺) = ( I ↾ 𝐴)))

Proof of Theorem f1eqcocnvOLD
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1cocnv1 6814 . . . 4 (𝐹:𝐴1-1𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
2 coeq2 5814 . . . . 5 (𝐹 = 𝐺 → (𝐹𝐹) = (𝐹𝐺))
32eqeq1d 2738 . . . 4 (𝐹 = 𝐺 → ((𝐹𝐹) = ( I ↾ 𝐴) ↔ (𝐹𝐺) = ( I ↾ 𝐴)))
41, 3syl5ibcom 244 . . 3 (𝐹:𝐴1-1𝐵 → (𝐹 = 𝐺 → (𝐹𝐺) = ( I ↾ 𝐴)))
54adantr 481 . 2 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝐹 = 𝐺 → (𝐹𝐺) = ( I ↾ 𝐴)))
6 f1fn 6739 . . . . . . 7 (𝐺:𝐴1-1𝐵𝐺 Fn 𝐴)
76adantl 482 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → 𝐺 Fn 𝐴)
87adantr 481 . . . . 5 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) → 𝐺 Fn 𝐴)
9 f1fn 6739 . . . . . . 7 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
109adantr 481 . . . . . 6 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → 𝐹 Fn 𝐴)
1110adantr 481 . . . . 5 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) → 𝐹 Fn 𝐴)
12 equid 2015 . . . . . . . . . 10 𝑥 = 𝑥
13 resieq 5948 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐴) → (𝑥( I ↾ 𝐴)𝑥𝑥 = 𝑥))
1412, 13mpbiri 257 . . . . . . . . 9 ((𝑥𝐴𝑥𝐴) → 𝑥( I ↾ 𝐴)𝑥)
1514anidms 567 . . . . . . . 8 (𝑥𝐴𝑥( I ↾ 𝐴)𝑥)
1615adantl 482 . . . . . . 7 ((((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) ∧ 𝑥𝐴) → 𝑥( I ↾ 𝐴)𝑥)
17 breq 5107 . . . . . . . 8 ((𝐹𝐺) = ( I ↾ 𝐴) → (𝑥(𝐹𝐺)𝑥𝑥( I ↾ 𝐴)𝑥))
1817ad2antlr 725 . . . . . . 7 ((((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) ∧ 𝑥𝐴) → (𝑥(𝐹𝐺)𝑥𝑥( I ↾ 𝐴)𝑥))
1916, 18mpbird 256 . . . . . 6 ((((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) ∧ 𝑥𝐴) → 𝑥(𝐹𝐺)𝑥)
20 fnfun 6602 . . . . . . . . . . . . . . 15 (𝐺 Fn 𝐴 → Fun 𝐺)
217, 20syl 17 . . . . . . . . . . . . . 14 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → Fun 𝐺)
22 fndm 6605 . . . . . . . . . . . . . . . . 17 (𝐺 Fn 𝐴 → dom 𝐺 = 𝐴)
237, 22syl 17 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → dom 𝐺 = 𝐴)
2423eleq2d 2823 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝑥 ∈ dom 𝐺𝑥𝐴))
2524biimpar 478 . . . . . . . . . . . . . 14 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → 𝑥 ∈ dom 𝐺)
26 funopfvb 6898 . . . . . . . . . . . . . 14 ((Fun 𝐺𝑥 ∈ dom 𝐺) → ((𝐺𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
2721, 25, 26syl2an2r 683 . . . . . . . . . . . . 13 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → ((𝐺𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
2827bicomd 222 . . . . . . . . . . . 12 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ↔ (𝐺𝑥) = 𝑦))
29 df-br 5106 . . . . . . . . . . . 12 (𝑥𝐺𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)
30 eqcom 2743 . . . . . . . . . . . 12 (𝑦 = (𝐺𝑥) ↔ (𝐺𝑥) = 𝑦)
3128, 29, 303bitr4g 313 . . . . . . . . . . 11 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑥𝐺𝑦𝑦 = (𝐺𝑥)))
3231biimpd 228 . . . . . . . . . 10 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑥𝐺𝑦𝑦 = (𝐺𝑥)))
33 df-br 5106 . . . . . . . . . . . . 13 (𝑥𝐹𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹)
34 fnfun 6602 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → Fun 𝐹)
3510, 34syl 17 . . . . . . . . . . . . . 14 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → Fun 𝐹)
36 fndm 6605 . . . . . . . . . . . . . . . . 17 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3710, 36syl 17 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → dom 𝐹 = 𝐴)
3837eleq2d 2823 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝑥 ∈ dom 𝐹𝑥𝐴))
3938biimpar 478 . . . . . . . . . . . . . 14 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → 𝑥 ∈ dom 𝐹)
40 funopfvb 6898 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
4135, 39, 40syl2an2r 683 . . . . . . . . . . . . 13 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → ((𝐹𝑥) = 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐹))
4233, 41bitr4id 289 . . . . . . . . . . . 12 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑥𝐹𝑦 ↔ (𝐹𝑥) = 𝑦))
43 vex 3449 . . . . . . . . . . . . 13 𝑦 ∈ V
44 vex 3449 . . . . . . . . . . . . 13 𝑥 ∈ V
4543, 44brcnv 5838 . . . . . . . . . . . 12 (𝑦𝐹𝑥𝑥𝐹𝑦)
46 eqcom 2743 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
4742, 45, 463bitr4g 313 . . . . . . . . . . 11 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑦𝐹𝑥𝑦 = (𝐹𝑥)))
4847biimpd 228 . . . . . . . . . 10 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑦𝐹𝑥𝑦 = (𝐹𝑥)))
4932, 48anim12d 609 . . . . . . . . 9 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → ((𝑥𝐺𝑦𝑦𝐹𝑥) → (𝑦 = (𝐺𝑥) ∧ 𝑦 = (𝐹𝑥))))
5049eximdv 1920 . . . . . . . 8 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (∃𝑦(𝑥𝐺𝑦𝑦𝐹𝑥) → ∃𝑦(𝑦 = (𝐺𝑥) ∧ 𝑦 = (𝐹𝑥))))
5144, 44brco 5826 . . . . . . . 8 (𝑥(𝐹𝐺)𝑥 ↔ ∃𝑦(𝑥𝐺𝑦𝑦𝐹𝑥))
52 fvex 6855 . . . . . . . . 9 (𝐺𝑥) ∈ V
5352eqvinc 3599 . . . . . . . 8 ((𝐺𝑥) = (𝐹𝑥) ↔ ∃𝑦(𝑦 = (𝐺𝑥) ∧ 𝑦 = (𝐹𝑥)))
5450, 51, 533imtr4g 295 . . . . . . 7 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ 𝑥𝐴) → (𝑥(𝐹𝐺)𝑥 → (𝐺𝑥) = (𝐹𝑥)))
5554adantlr 713 . . . . . 6 ((((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) ∧ 𝑥𝐴) → (𝑥(𝐹𝐺)𝑥 → (𝐺𝑥) = (𝐹𝑥)))
5619, 55mpd 15 . . . . 5 ((((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) ∧ 𝑥𝐴) → (𝐺𝑥) = (𝐹𝑥))
578, 11, 56eqfnfvd 6985 . . . 4 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) → 𝐺 = 𝐹)
5857eqcomd 2742 . . 3 (((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) ∧ (𝐹𝐺) = ( I ↾ 𝐴)) → 𝐹 = 𝐺)
5958ex 413 . 2 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → ((𝐹𝐺) = ( I ↾ 𝐴) → 𝐹 = 𝐺))
605, 59impbid 211 1 ((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝐹 = 𝐺 ↔ (𝐹𝐺) = ( I ↾ 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  cop 4592   class class class wbr 5105   I cid 5530  ccnv 5632  dom cdm 5633  cres 5635  ccom 5637  Fun wfun 6490   Fn wfn 6491  1-1wf1 6493  cfv 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator