Metamath Proof Explorer


Theorem f1eqcocnvOLD

Description: Obsolete version of f1eqcocnv as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion f1eqcocnvOLD ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 f1cocnv1 ( 𝐹 : 𝐴1-1𝐵 → ( 𝐹𝐹 ) = ( I ↾ 𝐴 ) )
2 coeq2 ( 𝐹 = 𝐺 → ( 𝐹𝐹 ) = ( 𝐹𝐺 ) )
3 2 eqeq1d ( 𝐹 = 𝐺 → ( ( 𝐹𝐹 ) = ( I ↾ 𝐴 ) ↔ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) )
4 1 3 syl5ibcom ( 𝐹 : 𝐴1-1𝐵 → ( 𝐹 = 𝐺 → ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) )
5 4 adantr ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( 𝐹 = 𝐺 → ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) )
6 f1fn ( 𝐺 : 𝐴1-1𝐵𝐺 Fn 𝐴 )
7 6 adantl ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → 𝐺 Fn 𝐴 )
8 7 adantr ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐺 Fn 𝐴 )
9 f1fn ( 𝐹 : 𝐴1-1𝐵𝐹 Fn 𝐴 )
10 9 adantr ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → 𝐹 Fn 𝐴 )
11 10 adantr ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐹 Fn 𝐴 )
12 equid 𝑥 = 𝑥
13 resieq ( ( 𝑥𝐴𝑥𝐴 ) → ( 𝑥 ( I ↾ 𝐴 ) 𝑥𝑥 = 𝑥 ) )
14 12 13 mpbiri ( ( 𝑥𝐴𝑥𝐴 ) → 𝑥 ( I ↾ 𝐴 ) 𝑥 )
15 14 anidms ( 𝑥𝐴𝑥 ( I ↾ 𝐴 ) 𝑥 )
16 15 adantl ( ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥𝐴 ) → 𝑥 ( I ↾ 𝐴 ) 𝑥 )
17 breq ( ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) → ( 𝑥 ( 𝐹𝐺 ) 𝑥𝑥 ( I ↾ 𝐴 ) 𝑥 ) )
18 17 ad2antlr ( ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ( 𝐹𝐺 ) 𝑥𝑥 ( I ↾ 𝐴 ) 𝑥 ) )
19 16 18 mpbird ( ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥𝐴 ) → 𝑥 ( 𝐹𝐺 ) 𝑥 )
20 fnfun ( 𝐺 Fn 𝐴 → Fun 𝐺 )
21 7 20 syl ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → Fun 𝐺 )
22 fndm ( 𝐺 Fn 𝐴 → dom 𝐺 = 𝐴 )
23 7 22 syl ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → dom 𝐺 = 𝐴 )
24 23 eleq2d ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( 𝑥 ∈ dom 𝐺𝑥𝐴 ) )
25 24 biimpar ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → 𝑥 ∈ dom 𝐺 )
26 funopfvb ( ( Fun 𝐺𝑥 ∈ dom 𝐺 ) → ( ( 𝐺𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
27 21 25 26 syl2an2r ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
28 27 bicomd ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ↔ ( 𝐺𝑥 ) = 𝑦 ) )
29 df-br ( 𝑥 𝐺 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 )
30 eqcom ( 𝑦 = ( 𝐺𝑥 ) ↔ ( 𝐺𝑥 ) = 𝑦 )
31 28 29 30 3bitr4g ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑥 𝐺 𝑦𝑦 = ( 𝐺𝑥 ) ) )
32 31 biimpd ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑥 𝐺 𝑦𝑦 = ( 𝐺𝑥 ) ) )
33 df-br ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
34 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
35 10 34 syl ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → Fun 𝐹 )
36 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
37 10 36 syl ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → dom 𝐹 = 𝐴 )
38 37 eleq2d ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( 𝑥 ∈ dom 𝐹𝑥𝐴 ) )
39 38 biimpar ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → 𝑥 ∈ dom 𝐹 )
40 funopfvb ( ( Fun 𝐹𝑥 ∈ dom 𝐹 ) → ( ( 𝐹𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
41 35 39 40 syl2an2r ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
42 33 41 bitr4id ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑥 𝐹 𝑦 ↔ ( 𝐹𝑥 ) = 𝑦 ) )
43 vex 𝑦 ∈ V
44 vex 𝑥 ∈ V
45 43 44 brcnv ( 𝑦 𝐹 𝑥𝑥 𝐹 𝑦 )
46 eqcom ( 𝑦 = ( 𝐹𝑥 ) ↔ ( 𝐹𝑥 ) = 𝑦 )
47 42 45 46 3bitr4g ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑦 𝐹 𝑥𝑦 = ( 𝐹𝑥 ) ) )
48 47 biimpd ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑦 𝐹 𝑥𝑦 = ( 𝐹𝑥 ) ) )
49 32 48 anim12d ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( ( 𝑥 𝐺 𝑦𝑦 𝐹 𝑥 ) → ( 𝑦 = ( 𝐺𝑥 ) ∧ 𝑦 = ( 𝐹𝑥 ) ) ) )
50 49 eximdv ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( ∃ 𝑦 ( 𝑥 𝐺 𝑦𝑦 𝐹 𝑥 ) → ∃ 𝑦 ( 𝑦 = ( 𝐺𝑥 ) ∧ 𝑦 = ( 𝐹𝑥 ) ) ) )
51 44 44 brco ( 𝑥 ( 𝐹𝐺 ) 𝑥 ↔ ∃ 𝑦 ( 𝑥 𝐺 𝑦𝑦 𝐹 𝑥 ) )
52 fvex ( 𝐺𝑥 ) ∈ V
53 52 eqvinc ( ( 𝐺𝑥 ) = ( 𝐹𝑥 ) ↔ ∃ 𝑦 ( 𝑦 = ( 𝐺𝑥 ) ∧ 𝑦 = ( 𝐹𝑥 ) ) )
54 50 51 53 3imtr4g ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ 𝑥𝐴 ) → ( 𝑥 ( 𝐹𝐺 ) 𝑥 → ( 𝐺𝑥 ) = ( 𝐹𝑥 ) ) )
55 54 adantlr ( ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ( 𝐹𝐺 ) 𝑥 → ( 𝐺𝑥 ) = ( 𝐹𝑥 ) ) )
56 19 55 mpd ( ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) = ( 𝐹𝑥 ) )
57 8 11 56 eqfnfvd ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐺 = 𝐹 )
58 57 eqcomd ( ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) ∧ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) → 𝐹 = 𝐺 )
59 58 ex ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) → 𝐹 = 𝐺 ) )
60 5 59 impbid ( ( 𝐹 : 𝐴1-1𝐵𝐺 : 𝐴1-1𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐹𝐺 ) = ( I ↾ 𝐴 ) ) )