Metamath Proof Explorer

Theorem fnunres1

Description: Restriction of a disjoint union to the domain of the first function. (Contributed by Thierry Arnoux, 9-Dec-2021)

Ref Expression
Assertion fnunres1 ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
2 1 3ad2ant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → dom 𝐹 = 𝐴 )
3 2 reseq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ dom 𝐹 ) = ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) )
4 fnrel ⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
5 4 3ad2ant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → Rel 𝐹 )
6 fndm ⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
7 6 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → dom 𝐺 = 𝐵 )
8 2 7 ineq12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐵 ) )
9 simp3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
10 8 9 eqtrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ )
11 relresdm1 ⊢ ( ( Rel 𝐹 ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ dom 𝐹 ) = 𝐹 )
12 5 10 11 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ dom 𝐹 ) = 𝐹 )
13 3 12 eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )