Theorem unfunc ≪ | index | src | ≫ 

theorem unfunc (A1 A2 B F1 F2: set) (G: wff):
  $ G -> A1 i^i A2 == 0 $ >
  $ G -> func F1 A1 B $ >
  $ G -> func F2 A2 B $ >
  $ G -> func (F1 u. F2) (A1 u. A2) B $;
StepHypRefExpression
1 unisf 
Dom F1 i^i Dom F2 == 0 -> (isfun (F1 u. F2) <-> isfun F1 /\ isfun F2)
2 funcdm 
func F1 A1 B -> Dom F1 == A1
3 hyp h1 
G -> func F1 A1 B
4 2, 3 syl 
G -> Dom F1 == A1
5 funcdm 
func F2 A2 B -> Dom F2 == A2
6 hyp h2 
G -> func F2 A2 B
7 5, 6 syl 
G -> Dom F2 == A2
8 4, 7 ineqd 
G -> Dom F1 i^i Dom F2 == A1 i^i A2
9 hyp h0 
G -> A1 i^i A2 == 0
10 8, 9 eqstrd 
G -> Dom F1 i^i Dom F2 == 0
11 1, 10 syl 
G -> (isfun (F1 u. F2) <-> isfun F1 /\ isfun F2)
12 funcisf 
func F1 A1 B -> isfun F1
13 12, 3 syl 
G -> isfun F1
14 funcisf 
func F2 A2 B -> isfun F2
15 14, 6 syl 
G -> isfun F2
16 13, 15 iand 
G -> isfun F1 /\ isfun F2
17 11, 16 mpbird 
G -> isfun (F1 u. F2)
18 dmun 
Dom (F1 u. F2) == Dom F1 u. Dom F2
19 4, 7 uneqd 
G -> Dom F1 u. Dom F2 == A1 u. A2
20 18, 19 syl5eqs 
G -> Dom (F1 u. F2) == A1 u. A2
21 17, 20 iand 
G -> isfun (F1 u. F2) /\ Dom (F1 u. F2) == A1 u. A2
22 sseq1 
Ran (F1 u. F2) == Ran F1 u. Ran F2 -> (Ran (F1 u. F2) C_ B <-> Ran F1 u. Ran F2 C_ B)
23 rnun 
Ran (F1 u. F2) == Ran F1 u. Ran F2
24 22, 23 ax_mp 
Ran (F1 u. F2) C_ B <-> Ran F1 u. Ran F2 C_ B
25 unss 
Ran F1 u. Ran F2 C_ B <-> Ran F1 C_ B /\ Ran F2 C_ B
26 funcrn 
func F1 A1 B -> Ran F1 C_ B
27 26, 3 syl 
G -> Ran F1 C_ B
28 funcrn 
func F2 A2 B -> Ran F2 C_ B
29 28, 6 syl 
G -> Ran F2 C_ B
30 27, 29 iand 
G -> Ran F1 C_ B /\ Ran F2 C_ B
31 25, 30 sylibr 
G -> Ran F1 u. Ran F2 C_ B
32 24, 31 sylibr 
G -> Ran (F1 u. F2) C_ B
33 21, 32 iand 
G -> isfun (F1 u. F2) /\ Dom (F1 u. F2) == A1 u. A2 /\ Ran (F1 u. F2) C_ B
34 33 conv func 
G -> func (F1 u. F2) (A1 u. A2) B

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)