Metamath Proof Explorer


Theorem resf1o

Description: Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017)

Ref Expression
Hypotheses resf1o.1 𝑋 = { 𝑓 ∈ ( 𝐵m 𝐴 ) ∣ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 }
resf1o.2 𝐹 = ( 𝑓𝑋 ↦ ( 𝑓𝐶 ) )
Assertion resf1o ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) → 𝐹 : 𝑋1-1-onto→ ( 𝐵m 𝐶 ) )

Proof

Step Hyp Ref Expression
1 resf1o.1 𝑋 = { 𝑓 ∈ ( 𝐵m 𝐴 ) ∣ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 }
2 resf1o.2 𝐹 = ( 𝑓𝑋 ↦ ( 𝑓𝐶 ) )
3 resexg ( 𝑓𝑋 → ( 𝑓𝐶 ) ∈ V )
4 3 adantl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ 𝑓𝑋 ) → ( 𝑓𝐶 ) ∈ V )
5 simpr ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑔 ∈ ( 𝐵m 𝐶 ) ) → 𝑔 ∈ ( 𝐵m 𝐶 ) )
6 difexg ( 𝐴𝑉 → ( 𝐴𝐶 ) ∈ V )
7 6 3ad2ant1 ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → ( 𝐴𝐶 ) ∈ V )
8 snex { 𝑍 } ∈ V
9 xpexg ( ( ( 𝐴𝐶 ) ∈ V ∧ { 𝑍 } ∈ V ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) ∈ V )
10 7 8 9 sylancl ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) ∈ V )
11 10 adantr ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑔 ∈ ( 𝐵m 𝐶 ) ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) ∈ V )
12 unexg ( ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ ( ( 𝐴𝐶 ) × { 𝑍 } ) ∈ V ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ∈ V )
13 5 11 12 syl2anc ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑔 ∈ ( 𝐵m 𝐶 ) ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ∈ V )
14 13 adantlr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ 𝑔 ∈ ( 𝐵m 𝐶 ) ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ∈ V )
15 1 rabeq2i ( 𝑓𝑋 ↔ ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) )
16 15 anbi1i ( ( 𝑓𝑋𝑔 = ( 𝑓𝐶 ) ) ↔ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) )
17 simprr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑔 = ( 𝑓𝐶 ) )
18 simprll ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑓 ∈ ( 𝐵m 𝐴 ) )
19 elmapi ( 𝑓 ∈ ( 𝐵m 𝐴 ) → 𝑓 : 𝐴𝐵 )
20 18 19 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑓 : 𝐴𝐵 )
21 simp3 ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → 𝐶𝐴 )
22 21 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝐶𝐴 )
23 20 22 fssresd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓𝐶 ) : 𝐶𝐵 )
24 simp2 ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → 𝐵𝑊 )
25 simp1 ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → 𝐴𝑉 )
26 25 21 ssexd ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → 𝐶 ∈ V )
27 elmapg ( ( 𝐵𝑊𝐶 ∈ V ) → ( ( 𝑓𝐶 ) ∈ ( 𝐵m 𝐶 ) ↔ ( 𝑓𝐶 ) : 𝐶𝐵 ) )
28 24 26 27 syl2anc ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) → ( ( 𝑓𝐶 ) ∈ ( 𝐵m 𝐶 ) ↔ ( 𝑓𝐶 ) : 𝐶𝐵 ) )
29 28 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( ( 𝑓𝐶 ) ∈ ( 𝐵m 𝐶 ) ↔ ( 𝑓𝐶 ) : 𝐶𝐵 ) )
30 23 29 mpbird ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓𝐶 ) ∈ ( 𝐵m 𝐶 ) )
31 17 30 eqeltrd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑔 ∈ ( 𝐵m 𝐶 ) )
32 undif ( 𝐶𝐴 ↔ ( 𝐶 ∪ ( 𝐴𝐶 ) ) = 𝐴 )
33 32 biimpi ( 𝐶𝐴 → ( 𝐶 ∪ ( 𝐴𝐶 ) ) = 𝐴 )
34 33 reseq2d ( 𝐶𝐴 → ( 𝑓 ↾ ( 𝐶 ∪ ( 𝐴𝐶 ) ) ) = ( 𝑓𝐴 ) )
35 22 34 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓 ↾ ( 𝐶 ∪ ( 𝐴𝐶 ) ) ) = ( 𝑓𝐴 ) )
36 ffn ( 𝑓 : 𝐴𝐵𝑓 Fn 𝐴 )
37 fnresdm ( 𝑓 Fn 𝐴 → ( 𝑓𝐴 ) = 𝑓 )
38 20 36 37 3syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓𝐴 ) = 𝑓 )
39 35 38 eqtr2d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑓 = ( 𝑓 ↾ ( 𝐶 ∪ ( 𝐴𝐶 ) ) ) )
40 resundi ( 𝑓 ↾ ( 𝐶 ∪ ( 𝐴𝐶 ) ) ) = ( ( 𝑓𝐶 ) ∪ ( 𝑓 ↾ ( 𝐴𝐶 ) ) )
41 39 40 eqtrdi ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑓 = ( ( 𝑓𝐶 ) ∪ ( 𝑓 ↾ ( 𝐴𝐶 ) ) ) )
42 17 eqcomd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓𝐶 ) = 𝑔 )
43 simprlr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 )
44 25 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝐴𝑉 )
45 simplr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑍𝐵 )
46 eqid ( 𝐵 ∖ { 𝑍 } ) = ( 𝐵 ∖ { 𝑍 } )
47 46 ffs2 ( ( 𝐴𝑉𝑍𝐵𝑓 : 𝐴𝐵 ) → ( 𝑓 supp 𝑍 ) = ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) )
48 44 45 20 47 syl3anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓 supp 𝑍 ) = ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) )
49 sseqin2 ( 𝐶𝐴 ↔ ( 𝐴𝐶 ) = 𝐶 )
50 49 biimpi ( 𝐶𝐴 → ( 𝐴𝐶 ) = 𝐶 )
51 22 50 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝐴𝐶 ) = 𝐶 )
52 43 48 51 3sstr4d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓 supp 𝑍 ) ⊆ ( 𝐴𝐶 ) )
53 simpl ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → 𝑓 ∈ ( 𝐵m 𝐴 ) )
54 53 19 36 3syl ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → 𝑓 Fn 𝐴 )
55 inundif ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) = 𝐴
56 55 fneq2i ( 𝑓 Fn ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) ↔ 𝑓 Fn 𝐴 )
57 54 56 sylibr ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → 𝑓 Fn ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) )
58 vex 𝑓 ∈ V
59 58 a1i ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → 𝑓 ∈ V )
60 simpr ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → 𝑍𝐵 )
61 inindif ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅
62 61 a1i ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅ )
63 fnsuppres ( ( 𝑓 Fn ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) ∧ ( 𝑓 ∈ V ∧ 𝑍𝐵 ) ∧ ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅ ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 𝐴𝐶 ) ↔ ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
64 57 59 60 62 63 syl121anc ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ 𝑍𝐵 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 𝐴𝐶 ) ↔ ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
65 18 45 64 syl2anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 𝐴𝐶 ) ↔ ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
66 52 65 mpbid ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( ( 𝐴𝐶 ) × { 𝑍 } ) )
67 42 66 uneq12d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( ( 𝑓𝐶 ) ∪ ( 𝑓 ↾ ( 𝐴𝐶 ) ) ) = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
68 41 67 eqtrd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
69 31 68 jca ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ) → ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) )
70 24 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝐵𝑊 )
71 25 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝐴𝑉 )
72 elmapi ( 𝑔 ∈ ( 𝐵m 𝐶 ) → 𝑔 : 𝐶𝐵 )
73 72 ad2antrl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑔 : 𝐶𝐵 )
74 simplr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑍𝐵 )
75 fconst6g ( 𝑍𝐵 → ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ 𝐵 )
76 74 75 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ 𝐵 )
77 disjdif ( 𝐶 ∩ ( 𝐴𝐶 ) ) = ∅
78 77 a1i ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝐶 ∩ ( 𝐴𝐶 ) ) = ∅ )
79 fun2 ( ( ( 𝑔 : 𝐶𝐵 ∧ ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴𝐶 ) ) = ∅ ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) : ( 𝐶 ∪ ( 𝐴𝐶 ) ) ⟶ 𝐵 )
80 73 76 78 79 syl21anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) : ( 𝐶 ∪ ( 𝐴𝐶 ) ) ⟶ 𝐵 )
81 simprr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
82 81 eqcomd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) = 𝑓 )
83 21 ad2antrr ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝐶𝐴 )
84 83 33 syl ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝐶 ∪ ( 𝐴𝐶 ) ) = 𝐴 )
85 82 84 feq12d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) : ( 𝐶 ∪ ( 𝐴𝐶 ) ) ⟶ 𝐵𝑓 : 𝐴𝐵 ) )
86 80 85 mpbid ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑓 : 𝐴𝐵 )
87 elmapg ( ( 𝐵𝑊𝐴𝑉 ) → ( 𝑓 ∈ ( 𝐵m 𝐴 ) ↔ 𝑓 : 𝐴𝐵 ) )
88 87 biimpar ( ( ( 𝐵𝑊𝐴𝑉 ) ∧ 𝑓 : 𝐴𝐵 ) → 𝑓 ∈ ( 𝐵m 𝐴 ) )
89 70 71 86 88 syl21anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑓 ∈ ( 𝐵m 𝐴 ) )
90 71 74 86 47 syl3anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑓 supp 𝑍 ) = ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) )
91 81 adantr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) )
92 91 fveq1d ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( 𝑓𝑥 ) = ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ‘ 𝑥 ) )
93 73 adantr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑔 : 𝐶𝐵 )
94 93 ffnd ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑔 Fn 𝐶 )
95 fconstg ( 𝑍𝐵 → ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ { 𝑍 } )
96 95 ad3antlr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ { 𝑍 } )
97 96 ffnd ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝐴𝐶 ) × { 𝑍 } ) Fn ( 𝐴𝐶 ) )
98 77 a1i ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( 𝐶 ∩ ( 𝐴𝐶 ) ) = ∅ )
99 simpr ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑥 ∈ ( 𝐴𝐶 ) )
100 fvun2 ( ( 𝑔 Fn 𝐶 ∧ ( ( 𝐴𝐶 ) × { 𝑍 } ) Fn ( 𝐴𝐶 ) ∧ ( ( 𝐶 ∩ ( 𝐴𝐶 ) ) = ∅ ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) ) → ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ‘ 𝑥 ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ‘ 𝑥 ) )
101 94 97 98 99 100 syl112anc ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ‘ 𝑥 ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ‘ 𝑥 ) )
102 fvconst ( ( ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ { 𝑍 } ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ‘ 𝑥 ) = 𝑍 )
103 96 99 102 syl2anc ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ‘ 𝑥 ) = 𝑍 )
104 92 101 103 3eqtrd ( ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → ( 𝑓𝑥 ) = 𝑍 )
105 86 104 suppss ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑓 supp 𝑍 ) ⊆ 𝐶 )
106 90 105 eqsstrrd ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 )
107 81 reseq1d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑓𝐶 ) = ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ↾ 𝐶 ) )
108 res0 ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ∅ ) = ∅
109 res0 ( 𝑔 ↾ ∅ ) = ∅
110 108 109 eqtr4i ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ∅ ) = ( 𝑔 ↾ ∅ )
111 77 reseq2i ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ∅ )
112 77 reseq2i ( 𝑔 ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) = ( 𝑔 ↾ ∅ )
113 110 111 112 3eqtr4ri ( 𝑔 ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) )
114 113 a1i ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( 𝑔 ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) )
115 fresaunres1 ( ( 𝑔 : 𝐶𝐵 ∧ ( ( 𝐴𝐶 ) × { 𝑍 } ) : ( 𝐴𝐶 ) ⟶ 𝐵 ∧ ( 𝑔 ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) × { 𝑍 } ) ↾ ( 𝐶 ∩ ( 𝐴𝐶 ) ) ) ) → ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ↾ 𝐶 ) = 𝑔 )
116 73 76 114 115 syl3anc ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ↾ 𝐶 ) = 𝑔 )
117 107 116 eqtr2d ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → 𝑔 = ( 𝑓𝐶 ) )
118 89 106 117 jca31 ( ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) ∧ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) → ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) )
119 69 118 impbida ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) → ( ( ( 𝑓 ∈ ( 𝐵m 𝐴 ) ∧ ( 𝑓 “ ( 𝐵 ∖ { 𝑍 } ) ) ⊆ 𝐶 ) ∧ 𝑔 = ( 𝑓𝐶 ) ) ↔ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) )
120 16 119 syl5bb ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) → ( ( 𝑓𝑋𝑔 = ( 𝑓𝐶 ) ) ↔ ( 𝑔 ∈ ( 𝐵m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴𝐶 ) × { 𝑍 } ) ) ) ) )
121 2 4 14 120 f1od ( ( ( 𝐴𝑉𝐵𝑊𝐶𝐴 ) ∧ 𝑍𝐵 ) → 𝐹 : 𝑋1-1-onto→ ( 𝐵m 𝐶 ) )