Metamath Proof Explorer

Theorem fnsuppres

Description: Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppres ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 supp 𝑍 ) ⊆ 𝐴 ↔ ( 𝐹 ↾ 𝐵 ) = ( 𝐵 × { 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 fndm ⊢ ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) → dom 𝐹 = ( 𝐴 ∪ 𝐵 ) )
2 1 rabeqdv ⊢ ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) → { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } = { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
3 2 3ad2ant1 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } = { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
4 3 sseq1d ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ) )
5 unss ⊢ ( ( { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ∧ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ) ↔ ( { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ∪ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ) ⊆ 𝐴 )
6 ssrab2 ⊢ { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴
7 6 biantrur ⊢ ( { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ( { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ∧ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ) )
8 rabun2 ⊢ { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } = ( { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ∪ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
9 8 sseq1i ⊢ ( { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ( { 𝑎 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ∪ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ) ⊆ 𝐴 )
10 5 7 9 3bitr4ri ⊢ ( { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 )
11 rabss ⊢ ( { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 → 𝑎 ∈ 𝐴 ) )
12 fvres ⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
13 12 adantl ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
14 simp2r ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑍 ∈ 𝑉 )
15 fvconst2g ⊢ ( ( 𝑍 ∈ 𝑉 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) = 𝑍 )
16 14 15 sylan ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) = 𝑍 )
17 13 16 eqeq12d ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑎 ) = 𝑍 ) )
18 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑍 )
19 18 a1i ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ¬ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑍 ) )
20 id ⊢ ( 𝑎 ∈ 𝐵 → 𝑎 ∈ 𝐵 )
21 simp3 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
22 minel ⊢ ( ( 𝑎 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ¬ 𝑎 ∈ 𝐴 )
23 20 21 22 syl2anr ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ¬ 𝑎 ∈ 𝐴 )
24 mtt ⊢ ( ¬ 𝑎 ∈ 𝐴 → ( ¬ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 → 𝑎 ∈ 𝐴 ) ) )
25 23 24 syl ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ¬ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 → 𝑎 ∈ 𝐴 ) ) )
26 17 19 25 3bitr2rd ⊢ ( ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 → 𝑎 ∈ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
27 26 ralbidva ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 → 𝑎 ∈ 𝐴 ) ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
28 11 27 bitrid ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( { 𝑎 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
29 10 28 bitrid ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( { 𝑎 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
30 4 29 bitrd ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
31 fnfun ⊢ ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) → Fun 𝐹 )
32 31 3anim1i ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( Fun 𝐹 ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) )
33 32 3expb ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ) → ( Fun 𝐹 ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) )
34 suppval1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
35 33 34 syl ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝐹 supp 𝑍 ) = { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
36 35 3adant3 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 supp 𝑍 ) = { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } )
37 36 sseq1d ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 supp 𝑍 ) ⊆ 𝐴 ↔ { 𝑎 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑎 ) ≠ 𝑍 } ⊆ 𝐴 ) )
38 simp1 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐹 Fn ( 𝐴 ∪ 𝐵 ) )
39 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
40 39 a1i ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) )
41 fnssres ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
42 38 40 41 syl2anc ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ↾ 𝐵 ) Fn 𝐵 )
43 fnconstg ⊢ ( 𝑍 ∈ 𝑉 → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
44 43 adantl ⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
45 44 3ad2ant2 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
46 eqfnfv ⊢ ( ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ∧ ( 𝐵 × { 𝑍 } ) Fn 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐵 × { 𝑍 } ) ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
47 42 45 46 syl2anc ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ↾ 𝐵 ) = ( 𝐵 × { 𝑍 } ) ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑎 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑎 ) ) )
48 30 37 47 3bitr4d ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 supp 𝑍 ) ⊆ 𝐴 ↔ ( 𝐹 ↾ 𝐵 ) = ( 𝐵 × { 𝑍 } ) ) )