| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fococnv2 6874 | . . . 4
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | 
| 2 |  | cnveq 5884 | . . . . . 6
⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺) | 
| 3 | 2 | coeq2d 5873 | . . . . 5
⊢ (𝐹 = 𝐺 → (𝐹 ∘ ◡𝐹) = (𝐹 ∘ ◡𝐺)) | 
| 4 | 3 | eqeq1d 2739 | . . . 4
⊢ (𝐹 = 𝐺 → ((𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵) ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | 
| 5 | 1, 4 | syl5ibcom 245 | . . 3
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 = 𝐺 → (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | 
| 6 | 5 | adantr 480 | . 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 → (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | 
| 7 |  | fofn 6822 | . . . . 5
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) | 
| 8 | 7 | ad2antrr 726 | . . . 4
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) → 𝐹 Fn 𝐴) | 
| 9 |  | fofn 6822 | . . . . 5
⊢ (𝐺:𝐴–onto→𝐵 → 𝐺 Fn 𝐴) | 
| 10 | 9 | ad2antlr 727 | . . . 4
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) → 𝐺 Fn 𝐴) | 
| 11 | 9 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → 𝐺 Fn 𝐴) | 
| 12 |  | fnopfv 7095 | . . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐺‘𝑥)〉 ∈ 𝐺) | 
| 13 | 11, 12 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐺‘𝑥)〉 ∈ 𝐺) | 
| 14 |  | fvex 6919 | . . . . . . . . . . . . 13
⊢ (𝐺‘𝑥) ∈ V | 
| 15 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 16 | 14, 15 | brcnv 5893 | . . . . . . . . . . . 12
⊢ ((𝐺‘𝑥)◡𝐺𝑥 ↔ 𝑥𝐺(𝐺‘𝑥)) | 
| 17 |  | df-br 5144 | . . . . . . . . . . . 12
⊢ (𝑥𝐺(𝐺‘𝑥) ↔ 〈𝑥, (𝐺‘𝑥)〉 ∈ 𝐺) | 
| 18 | 16, 17 | bitri 275 | . . . . . . . . . . 11
⊢ ((𝐺‘𝑥)◡𝐺𝑥 ↔ 〈𝑥, (𝐺‘𝑥)〉 ∈ 𝐺) | 
| 19 | 13, 18 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥)◡𝐺𝑥) | 
| 20 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → 𝐹 Fn 𝐴) | 
| 21 |  | fnopfv 7095 | . . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) | 
| 22 | 20, 21 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) | 
| 23 |  | df-br 5144 | . . . . . . . . . . 11
⊢ (𝑥𝐹(𝐹‘𝑥) ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) | 
| 24 | 22, 23 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥𝐹(𝐹‘𝑥)) | 
| 25 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → ((𝐺‘𝑥)◡𝐺𝑦 ↔ (𝐺‘𝑥)◡𝐺𝑥)) | 
| 26 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦𝐹(𝐹‘𝑥) ↔ 𝑥𝐹(𝐹‘𝑥))) | 
| 27 | 25, 26 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (((𝐺‘𝑥)◡𝐺𝑦 ∧ 𝑦𝐹(𝐹‘𝑥)) ↔ ((𝐺‘𝑥)◡𝐺𝑥 ∧ 𝑥𝐹(𝐹‘𝑥)))) | 
| 28 | 15, 27 | spcev 3606 | . . . . . . . . . 10
⊢ (((𝐺‘𝑥)◡𝐺𝑥 ∧ 𝑥𝐹(𝐹‘𝑥)) → ∃𝑦((𝐺‘𝑥)◡𝐺𝑦 ∧ 𝑦𝐹(𝐹‘𝑥))) | 
| 29 | 19, 24, 28 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → ∃𝑦((𝐺‘𝑥)◡𝐺𝑦 ∧ 𝑦𝐹(𝐹‘𝑥))) | 
| 30 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V | 
| 31 | 14, 30 | brco 5881 | . . . . . . . . 9
⊢ ((𝐺‘𝑥)(𝐹 ∘ ◡𝐺)(𝐹‘𝑥) ↔ ∃𝑦((𝐺‘𝑥)◡𝐺𝑦 ∧ 𝑦𝐹(𝐹‘𝑥))) | 
| 32 | 29, 31 | sylibr 234 | . . . . . . . 8
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥)(𝐹 ∘ ◡𝐺)(𝐹‘𝑥)) | 
| 33 | 32 | adantlr 715 | . . . . . . 7
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥)(𝐹 ∘ ◡𝐺)(𝐹‘𝑥)) | 
| 34 |  | breq 5145 | . . . . . . . 8
⊢ ((𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵) → ((𝐺‘𝑥)(𝐹 ∘ ◡𝐺)(𝐹‘𝑥) ↔ (𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥))) | 
| 35 | 34 | ad2antlr 727 | . . . . . . 7
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥)(𝐹 ∘ ◡𝐺)(𝐹‘𝑥) ↔ (𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥))) | 
| 36 | 33, 35 | mpbid 232 | . . . . . 6
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥)) | 
| 37 |  | fof 6820 | . . . . . . . . . 10
⊢ (𝐺:𝐴–onto→𝐵 → 𝐺:𝐴⟶𝐵) | 
| 38 | 37 | adantl 481 | . . . . . . . . 9
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → 𝐺:𝐴⟶𝐵) | 
| 39 | 38 | ffvelcdmda 7104 | . . . . . . . 8
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵) | 
| 40 |  | fof 6820 | . . . . . . . . . 10
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) | 
| 41 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → 𝐹:𝐴⟶𝐵) | 
| 42 | 41 | ffvelcdmda 7104 | . . . . . . . 8
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | 
| 43 |  | resieq 6008 | . . . . . . . 8
⊢ (((𝐺‘𝑥) ∈ 𝐵 ∧ (𝐹‘𝑥) ∈ 𝐵) → ((𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥) ↔ (𝐺‘𝑥) = (𝐹‘𝑥))) | 
| 44 | 39, 42, 43 | syl2anc 584 | . . . . . . 7
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥) ↔ (𝐺‘𝑥) = (𝐹‘𝑥))) | 
| 45 | 44 | adantlr 715 | . . . . . 6
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥)( I ↾ 𝐵)(𝐹‘𝑥) ↔ (𝐺‘𝑥) = (𝐹‘𝑥))) | 
| 46 | 36, 45 | mpbid 232 | . . . . 5
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘𝑥)) | 
| 47 | 46 | eqcomd 2743 | . . . 4
⊢ ((((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) | 
| 48 | 8, 10, 47 | eqfnfvd 7054 | . . 3
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) ∧ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵)) → 𝐹 = 𝐺) | 
| 49 | 48 | ex 412 | . 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → ((𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵) → 𝐹 = 𝐺)) | 
| 50 | 6, 49 | impbid 212 | 1
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) |