Step | Hyp | Ref
| Expression |
1 | | f1cocnv1 5099 |
. . . 4
⊢ (𝐹:A–1-1→B →
(◡𝐹 ∘ 𝐹) = ( I ↾ A)) |
2 | | coeq2 4437 |
. . . . 5
⊢ (𝐹 = 𝐺 → (◡𝐹 ∘ 𝐹) = (◡𝐹 ∘ 𝐺)) |
3 | 2 | eqeq1d 2045 |
. . . 4
⊢ (𝐹 = 𝐺 → ((◡𝐹 ∘ 𝐹) = ( I ↾ A) ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ A))) |
4 | 1, 3 | syl5ibcom 144 |
. . 3
⊢ (𝐹:A–1-1→B →
(𝐹 = 𝐺 → (◡𝐹 ∘ 𝐺) = ( I ↾ A))) |
5 | 4 | adantr 261 |
. 2
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
(𝐹 = 𝐺 → (◡𝐹 ∘ 𝐺) = ( I ↾ A))) |
6 | | f1fn 5036 |
. . . . . . 7
⊢ (𝐺:A–1-1→B →
𝐺 Fn A) |
7 | 6 | adantl 262 |
. . . . . 6
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
𝐺 Fn A) |
8 | 7 | adantr 261 |
. . . . 5
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐺 Fn A) |
9 | | f1fn 5036 |
. . . . . . 7
⊢ (𝐹:A–1-1→B →
𝐹 Fn A) |
10 | 9 | adantr 261 |
. . . . . 6
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
𝐹 Fn A) |
11 | 10 | adantr 261 |
. . . . 5
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐹 Fn A) |
12 | | equid 1586 |
. . . . . . . . . 10
⊢ x = x |
13 | | resieq 4565 |
. . . . . . . . . 10
⊢
((x ∈ A ∧ x ∈ A) →
(x( I ↾ A)x ↔
x = x)) |
14 | 12, 13 | mpbiri 157 |
. . . . . . . . 9
⊢
((x ∈ A ∧ x ∈ A) →
x( I ↾ A)x) |
15 | 14 | anidms 377 |
. . . . . . . 8
⊢ (x ∈ A → x( I
↾ A)x) |
16 | 15 | adantl 262 |
. . . . . . 7
⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → x( I
↾ A)x) |
17 | | breq 3757 |
. . . . . . . 8
⊢ ((◡𝐹 ∘ 𝐺) = ( I ↾ A) → (x(◡𝐹 ∘ 𝐺)x
↔ x( I ↾ A)x)) |
18 | 17 | ad2antlr 458 |
. . . . . . 7
⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x
↔ x( I ↾ A)x)) |
19 | 16, 18 | mpbird 156 |
. . . . . 6
⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → x(◡𝐹 ∘ 𝐺)x) |
20 | | vex 2554 |
. . . . . . . . . 10
⊢ x ∈
V |
21 | 20, 20 | brco 4449 |
. . . . . . . . 9
⊢ (x(◡𝐹 ∘ 𝐺)x
↔ ∃y(x𝐺y ∧ y◡𝐹x)) |
22 | | fnfun 4939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn A → Fun 𝐺) |
23 | 7, 22 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
Fun 𝐺) |
24 | 23 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → Fun
𝐺) |
25 | | fndm 4941 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 Fn A → dom 𝐺 = A) |
26 | 7, 25 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
dom 𝐺 = A) |
27 | 26 | eleq2d 2104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
(x ∈ dom
𝐺 ↔ x ∈ A)) |
28 | 27 | biimpar 281 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
x ∈ dom
𝐺) |
29 | | funopfvb 5160 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐺 ∧ x ∈ dom 𝐺) → ((𝐺‘x) = y ↔
〈x, y〉 ∈ 𝐺)) |
30 | 24, 28, 29 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
((𝐺‘x) = y ↔
〈x, y〉 ∈ 𝐺)) |
31 | 30 | bicomd 129 |
. . . . . . . . . . . . 13
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(〈x, y〉 ∈ 𝐺 ↔ (𝐺‘x) = y)) |
32 | | df-br 3756 |
. . . . . . . . . . . . 13
⊢ (x𝐺y ↔
〈x, y〉 ∈ 𝐺) |
33 | | eqcom 2039 |
. . . . . . . . . . . . 13
⊢ (y = (𝐺‘x) ↔ (𝐺‘x) = y) |
34 | 31, 32, 33 | 3bitr4g 212 |
. . . . . . . . . . . 12
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(x𝐺y ↔
y = (𝐺‘x))) |
35 | 34 | biimpd 132 |
. . . . . . . . . . 11
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(x𝐺y →
y = (𝐺‘x))) |
36 | | fnfun 4939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn A → Fun 𝐹) |
37 | 10, 36 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
Fun 𝐹) |
38 | 37 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) → Fun
𝐹) |
39 | | fndm 4941 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn A → dom 𝐹 = A) |
40 | 10, 39 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
dom 𝐹 = A) |
41 | 40 | eleq2d 2104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
(x ∈ dom
𝐹 ↔ x ∈ A)) |
42 | 41 | biimpar 281 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
x ∈ dom
𝐹) |
43 | | funopfvb 5160 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → ((𝐹‘x) = y ↔
〈x, y〉 ∈ 𝐹)) |
44 | 38, 42, 43 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
((𝐹‘x) = y ↔
〈x, y〉 ∈ 𝐹)) |
45 | | df-br 3756 |
. . . . . . . . . . . . . 14
⊢ (x𝐹y ↔
〈x, y〉 ∈ 𝐹) |
46 | 44, 45 | syl6rbbr 188 |
. . . . . . . . . . . . 13
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(x𝐹y ↔
(𝐹‘x) = y)) |
47 | | vex 2554 |
. . . . . . . . . . . . . 14
⊢ y ∈
V |
48 | 47, 20 | brcnv 4461 |
. . . . . . . . . . . . 13
⊢ (y◡𝐹x ↔ x𝐹y) |
49 | | eqcom 2039 |
. . . . . . . . . . . . 13
⊢ (y = (𝐹‘x) ↔ (𝐹‘x) = y) |
50 | 46, 48, 49 | 3bitr4g 212 |
. . . . . . . . . . . 12
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(y◡𝐹x ↔
y = (𝐹‘x))) |
51 | 50 | biimpd 132 |
. . . . . . . . . . 11
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(y◡𝐹x →
y = (𝐹‘x))) |
52 | 35, 51 | anim12d 318 |
. . . . . . . . . 10
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
((x𝐺y ∧ y◡𝐹x)
→ (y = (𝐺‘x) ∧ y = (𝐹‘x)))) |
53 | 52 | eximdv 1757 |
. . . . . . . . 9
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(∃y(x𝐺y ∧ y◡𝐹x) → ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x)))) |
54 | 21, 53 | syl5bi 141 |
. . . . . . . 8
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(x(◡𝐹 ∘ 𝐺)x
→ ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x)))) |
55 | 6 | anim1i 323 |
. . . . . . . . . 10
⊢ ((𝐺:A–1-1→B ∧ x ∈ A) →
(𝐺 Fn A ∧ x ∈ A)) |
56 | 55 | adantll 445 |
. . . . . . . . 9
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(𝐺 Fn A ∧ x ∈ A)) |
57 | | funfvex 5135 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ x ∈ dom 𝐺) → (𝐺‘x) ∈
V) |
58 | 57 | funfni 4942 |
. . . . . . . . 9
⊢ ((𝐺 Fn A ∧ x ∈ A) → (𝐺‘x) ∈
V) |
59 | | eqvincg 2662 |
. . . . . . . . 9
⊢ ((𝐺‘x) ∈ V →
((𝐺‘x) = (𝐹‘x) ↔ ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x)))) |
60 | 56, 58, 59 | 3syl 17 |
. . . . . . . 8
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
((𝐺‘x) = (𝐹‘x) ↔ ∃y(y = (𝐺‘x) ∧ y = (𝐹‘x)))) |
61 | 54, 60 | sylibrd 158 |
. . . . . . 7
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ x ∈ A) →
(x(◡𝐹 ∘ 𝐺)x
→ (𝐺‘x) = (𝐹‘x))) |
62 | 61 | adantlr 446 |
. . . . . 6
⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (x(◡𝐹 ∘ 𝐺)x
→ (𝐺‘x) = (𝐹‘x))) |
63 | 19, 62 | mpd 13 |
. . . . 5
⊢ ((((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) ∧ x ∈ A) → (𝐺‘x) = (𝐹‘x)) |
64 | 8, 11, 63 | eqfnfvd 5211 |
. . . 4
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐺 = 𝐹) |
65 | 64 | eqcomd 2042 |
. . 3
⊢ (((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) ∧ (◡𝐹 ∘ 𝐺) = ( I ↾ A)) → 𝐹 = 𝐺) |
66 | 65 | ex 108 |
. 2
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
((◡𝐹 ∘ 𝐺) = ( I ↾ A) → 𝐹 = 𝐺)) |
67 | 5, 66 | impbid 120 |
1
⊢ ((𝐹:A–1-1→B ∧ 𝐺:A–1-1→B) →
(𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ A))) |