Theorem func02 ≪ | index | src | ≫ 

theorem func02 (B F: set): $ func F 0 B <-> F == 0 $;
StepHypRefExpression
1 bitr 
(func F 0 B <-> F == 0 /\ Ran F C_ B) -> (F == 0 /\ Ran F C_ B <-> F == 0) -> (func F 0 B <-> F == 0)
2 bitr 
(isfun F /\ Dom F == 0 <-> isfun F /\ F == 0) -> (isfun F /\ F == 0 <-> F == 0) -> (isfun F /\ Dom F == 0 <-> F == 0)
3 dmeq0 
Dom F == 0 <-> F == 0
4 3 aneq2i 
isfun F /\ Dom F == 0 <-> isfun F /\ F == 0
5 2, 4 ax_mp 
(isfun F /\ F == 0 <-> F == 0) -> (isfun F /\ Dom F == 0 <-> F == 0)
6 bian1a 
(F == 0 -> isfun F) -> (isfun F /\ F == 0 <-> F == 0)
7 isf0 
isfun 0
8 isfeq 
F == 0 -> (isfun F <-> isfun 0)
9 7, 8 mpbiri 
F == 0 -> isfun F
10 6, 9 ax_mp 
isfun F /\ F == 0 <-> F == 0
11 5, 10 ax_mp 
isfun F /\ Dom F == 0 <-> F == 0
12 11 aneq1i 
isfun F /\ Dom F == 0 /\ Ran F C_ B <-> F == 0 /\ Ran F C_ B
13 12 conv func 
func F 0 B <-> F == 0 /\ Ran F C_ B
14 1, 13 ax_mp 
(F == 0 /\ Ran F C_ B <-> F == 0) -> (func F 0 B <-> F == 0)
15 bian2a 
(F == 0 -> Ran F C_ B) -> (F == 0 /\ Ran F C_ B <-> F == 0)
16 ss01 
0 C_ B
17 rneq0 
Ran F == 0 <-> F == 0
18 sseq1 
Ran F == 0 -> (Ran F C_ B <-> 0 C_ B)
19 17, 18 sylbir 
F == 0 -> (Ran F C_ B <-> 0 C_ B)
20 16, 19 mpbiri 
F == 0 -> Ran F C_ B
21 15, 20 ax_mp 
F == 0 /\ Ran F C_ B <-> F == 0
22 14, 21 ax_mp 
func F 0 B <-> F == 0

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)