This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 reqabi ⊢ ( 𝑓 ∈ 𝑋 ↔ ( 𝑓 ∈ ( 𝐵 ↑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 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 = ( 𝑓 ↾ 𝐶 ) ) ↔ ( 𝑔 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝑓 = ( 𝑔 ∪ ( ( 𝐴 ∖ 𝐶 ) × { 𝑍 } ) ) ) ) )
121 2 4 14 120 f1od ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴 ) ∧ 𝑍 ∈ 𝐵 ) → 𝐹 : 𝑋 –1-1-onto→ ( 𝐵 ↑m 𝐶 ) )