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 disjdifr ⊢ A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅
14 13 a1i ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → A ∖ C F -1 ⁡ D ∩ C F -1 ⁡ D = ∅
15 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
16 4 12 14 14 15 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
17 uncom ⊢ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D = C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D
18 5 10 prssd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D ⊆ A
19 undif ⊢ C F -1 ⁡ D ⊆ A ↔ C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D = A
20 18 19 sylib ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D ∪ A ∖ C F -1 ⁡ D = A
21 17 20 syl5eq ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D = A
22 21 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
23 16 22 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
24 21 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
25 23 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
26 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
27 2 25 26 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
28 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
29 1 28 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
30 27 29 sylibr ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G : A ⟶ 1-1 onto B
31 1 fveq1i ⊢ G ⁡ C = F ∘ I ↾ A ∖ C F -1 ⁡ D ∪ C F -1 ⁡ D F -1 ⁡ D C ⁡ C
32 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
33 25 32 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
34 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
35 33 5 34 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
36 31 35 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
37 fnresi ⊢ I ↾ A ∖ C F -1 ⁡ D Fn A ∖ C F -1 ⁡ D
38 37 a1i ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → I ↾ A ∖ C F -1 ⁡ D Fn A ∖ C F -1 ⁡ D
39 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
40 12 39 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D F -1 ⁡ D C Fn C F -1 ⁡ D
41 prid1g ⊢ C ∈ A → C ∈ C F -1 ⁡ D
42 5 41 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C ∈ C F -1 ⁡ D
43 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
44 38 40 14 42 43 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
45 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
46 12 45 syl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → Fun ⁡ C F -1 ⁡ D F -1 ⁡ D C
47 opex ⊢ C F -1 ⁡ D ∈ V
48 47 prid1 ⊢ C F -1 ⁡ D ∈ C F -1 ⁡ D F -1 ⁡ D C
49 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
50 46 48 49 mpisyl ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → C F -1 ⁡ D F -1 ⁡ D C ⁡ C = F -1 ⁡ D
51 44 50 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
52 51 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
53 f1ocnvfv2 ⊢ F : A ⟶ 1-1 onto B ∧ D ∈ B → F ⁡ F -1 ⁡ D = D
54 2 9 53 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → F ⁡ F -1 ⁡ D = D
55 52 54 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
56 36 55 eqtrd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G ⁡ C = D
57 30 56 jca ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ A ∧ D ∈ B → G : A ⟶ 1-1 onto B ∧ G ⁡ C = D