Metamath Proof Explorer

Theorem fveqf1o

Description: Given a bijection F , produce another bijection G which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypothesis fveqf1o.1 ⊢ G = F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C
Assertion fveqf1o ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G : A ⟶ 1-1 onto B ∧ G ⁡ C = D

Proof

Step Hyp Ref Expression
1 fveqf1o.1 ⊢ G = F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C
2 simp1 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F : A ⟶ 1-1 onto B
3 f1oi ⊢ I ↾ A ∖ C F -1 ⁡ D : A ∖ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D
4 3 a1i ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D : A ∖ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D
5 simp2 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C ∈ A
6 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
7 f1of ⊢ F -1 : B ⟶ 1-1 onto A → F -1 : B ⟶ A
8 2 6 7 3syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F -1 : B ⟶ A
9 simp3 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → D ∈ B
10 8 9 ffvelrnd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F -1 ⁡ D ∈ A
11 f1oprswap ⊢ C ∈ A ∧ F -1 ⁡ D ∈ A → C F -1 ⁡ D F -1 ⁡ D C : C F -1 ⁡ D ⟶ 1-1 onto C F -1 ⁡ D
12 5 10 11 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D F -1 ⁡ D C : C F -1 ⁡ D ⟶ 1-1 onto C F -1 ⁡ D
13 incom ⊢ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = C F -1 ⁡ D ∩ A ∖ C F -1 ⁡ D
14 disjdif ⊢ C F -1 ⁡ D ∩ A ∖ C F -1 ⁡ D = ∅
15 13 14 eqtri ⊢ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅
16 15 a1i ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅
17 f1oun ⊢ I ↾ A ∖ C F -1 ⁡ D : A ∖ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∧ C F -1 ⁡ D F -1 ⁡ D C : C F -1 ⁡ D ⟶ 1-1 onto C F -1 ⁡ D ∧ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅ ∧ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅ → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D
18 4 12 16 16 17 syl22anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D
19 uncom ⊢ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D = C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D
20 5 10 prssd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D ⊆ A
21 undif ⊢ C F -1 ⁡ D ⊆ A ↔ C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D = A
22 20 21 sylib ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D = A
23 19 22 syl5eq ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D = A
24 23 f1oeq2d ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D ↔ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D
25 18 24 mpbid ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D
26 23 f1oeq3d ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D ↔ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A
27 25 26 mpbid ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A
28 f1oco ⊢ F : A ⟶ 1-1 onto B ∧ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A → F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto B
29 2 27 28 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto B
30 f1oeq1 ⊢ G = F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C → G : A ⟶ 1-1 onto B ↔ F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto B
31 1 30 ax-mp ⊢ G : A ⟶ 1-1 onto B ↔ F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto B
32 29 31 sylibr ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G : A ⟶ 1-1 onto B
33 1 fveq1i ⊢ G ⁡ C = F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C
34 f1of ⊢ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ 1-1 onto A → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ A
35 27 34 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ A
36 fvco3 ⊢ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C : A ⟶ A ∧ C ∈ A → F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F ⁡ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C
37 35 5 36 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F ⁡ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C
38 33 37 syl5eq ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G ⁡ C = F ⁡ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C
39 fnresi ⊢ I ↾ A ∖ C F -1 ⁡ D Fn A ∖ C F -1 ⁡ D
40 39 a1i ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D Fn A ∖ C F -1 ⁡ D
41 f1ofn ⊢ C F -1 ⁡ D F -1 ⁡ D C : C F -1 ⁡ D ⟶ 1-1 onto C F -1 ⁡ D → C F -1 ⁡ D F -1 ⁡ D C Fn C F -1 ⁡ D
42 12 41 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D F -1 ⁡ D C Fn C F -1 ⁡ D
43 prid1g ⊢ C ∈ A → C ∈ C F -1 ⁡ D
44 5 43 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C ∈ C F -1 ⁡ D
45 fvun2 ⊢ I ↾ A ∖ C F -1 ⁡ D Fn A ∖ C F -1 ⁡ D ∧ C F -1 ⁡ D F -1 ⁡ D C Fn C F -1 ⁡ D ∧ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅ ∧ C ∈ C F -1 ⁡ D → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = C F -1 ⁡ D F -1 ⁡ D C ⁡ C
46 40 42 16 44 45 syl112anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = C F -1 ⁡ D F -1 ⁡ D C ⁡ C
47 f1ofun ⊢ C F -1 ⁡ D F -1 ⁡ D C : C F -1 ⁡ D ⟶ 1-1 onto C F -1 ⁡ D → Fun ⁡ C F -1 ⁡ D F -1 ⁡ D C
48 12 47 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → Fun ⁡ C F -1 ⁡ D F -1 ⁡ D C
49 opex ⊢ C F -1 ⁡ D ∈ V
50 49 prid1 ⊢ C F -1 ⁡ D ∈ C F -1 ⁡ D F -1 ⁡ D C
51 funopfv ⊢ Fun ⁡ C F -1 ⁡ D F -1 ⁡ D C → C F -1 ⁡ D ∈ C F -1 ⁡ D F -1 ⁡ D C → C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F -1 ⁡ D
52 48 50 51 mpisyl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F -1 ⁡ D
53 46 52 eqtrd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F -1 ⁡ D
54 53 fveq2d ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F ⁡ F -1 ⁡ D
55 f1ocnvfv2 ⊢ F : A ⟶ 1-1 onto B ∧ D ∈ B → F ⁡ F -1 ⁡ D = D
56 2 9 55 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ F -1 ⁡ D = D
57 54 56 eqtrd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C = D
58 38 57 eqtrd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G ⁡ C = D
59 32 58 jca ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G : A ⟶ 1-1 onto B ∧ G ⁡ C = D