Metamath Proof Explorer

Theorem funun

Description: The union of functions with disjoint domains is a function. Theorem 4.6 of Monk1 p. 43. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion funun ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → Fun ( 𝐹 ∪ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
2 funrel ⊢ ( Fun 𝐺 → Rel 𝐺 )
3 1 2 anim12i ⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( Rel 𝐹 ∧ Rel 𝐺 ) )
4 relun ⊢ ( Rel ( 𝐹 ∪ 𝐺 ) ↔ ( Rel 𝐹 ∧ Rel 𝐺 ) )
5 3 4 sylibr ⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Rel ( 𝐹 ∪ 𝐺 ) )
6 5 adantr ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → Rel ( 𝐹 ∪ 𝐺 ) )
7 elun ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) )
8 elun ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) )
9 7 8 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) )
10 anddi ⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ) ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ∨ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ↔ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ∨ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) )
11 9 10 bitri ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) ↔ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ∨ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) )
12 disj1 ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺 ) )
13 12 biimpi ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ∀ 𝑥 ( 𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺 ) )
14 13 19.21bi ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺 ) )
15 imnan ⊢ ( ( 𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺 ) ↔ ¬ ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) )
16 14 15 sylib ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) )
17 vex ⊢ 𝑥 ∈ V
18 vex ⊢ 𝑦 ∈ V
19 17 18 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹 )
20 vex ⊢ 𝑧 ∈ V
21 17 20 opeldm ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 )
22 19 21 anim12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺 ) )
23 16 22 nsyl ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) )
24 orel2 ⊢ ( ¬ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) )
25 23 24 syl ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ) )
26 14 con2d ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹 ) )
27 imnan ⊢ ( ( 𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹 ) ↔ ¬ ( 𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹 ) )
28 26 27 sylib ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ ( 𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹 ) )
29 17 18 opeldm ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺 )
30 17 20 opeldm ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹 )
31 29 30 anim12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( 𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹 ) )
32 28 31 nsyl ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
33 orel1 ⊢ ( ¬ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) )
34 32 33 syl ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) )
35 25 34 orim12d ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ∨ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) )
36 35 adantl ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ∨ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) )
37 11 36 syl5bi ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) ) )
38 dffun4 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) ) )
39 38 simprbi ⊢ ( Fun 𝐹 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
40 39 19.21bi ⊢ ( Fun 𝐹 → ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
41 40 19.21bbi ⊢ ( Fun 𝐹 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) → 𝑦 = 𝑧 ) )
42 dffun4 ⊢ ( Fun 𝐺 ↔ ( Rel 𝐺 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → 𝑦 = 𝑧 ) ) )
43 42 simprbi ⊢ ( Fun 𝐺 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → 𝑦 = 𝑧 ) )
44 43 19.21bi ⊢ ( Fun 𝐺 → ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → 𝑦 = 𝑧 ) )
45 44 19.21bbi ⊢ ( Fun 𝐺 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) → 𝑦 = 𝑧 ) )
46 41 45 jaao ⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → 𝑦 = 𝑧 ) )
47 46 adantr ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) ∨ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐺 ) ) → 𝑦 = 𝑧 ) )
48 37 47 syld ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) → 𝑦 = 𝑧 ) )
49 48 alrimiv ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) → 𝑦 = 𝑧 ) )
50 49 alrimivv ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) → 𝑦 = 𝑧 ) )
51 dffun4 ⊢ ( Fun ( 𝐹 ∪ 𝐺 ) ↔ ( Rel ( 𝐹 ∪ 𝐺 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐹 ∪ 𝐺 ) ) → 𝑦 = 𝑧 ) ) )
52 6 50 51 sylanbrc ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → Fun ( 𝐹 ∪ 𝐺 ) )