Theorem func03 ≪ | index | src | ≫ 

theorem func03 (A F: set): $ func F A 0 <-> F == 0 /\ A == 0 $;
StepHypRefExpression
1 bitr3 
(F == 0 /\ func F A 0 <-> func F A 0) -> (F == 0 /\ func F A 0 <-> F == 0 /\ A == 0) -> (func F A 0 <-> F == 0 /\ A == 0)
2 bian1a 
(func F A 0 -> F == 0) -> (F == 0 /\ func F A 0 <-> func F A 0)
3 rneq0 
Ran F == 0 <-> F == 0
4 ss02 
Ran F C_ 0 <-> Ran F == 0
5 funcrn 
func F A 0 -> Ran F C_ 0
6 4, 5 sylib 
func F A 0 -> Ran F == 0
7 3, 6 sylib 
func F A 0 -> F == 0
8 2, 7 ax_mp 
F == 0 /\ func F A 0 <-> func F A 0
9 1, 8 ax_mp 
(F == 0 /\ func F A 0 <-> F == 0 /\ A == 0) -> (func F A 0 <-> F == 0 /\ A == 0)
10 aneq2a 
(F == 0 -> (func F A 0 <-> A == 0)) -> (F == 0 /\ func F A 0 <-> F == 0 /\ A == 0)
11 bitr 
(isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> isfun 0 /\ Dom 0 == A) -> (isfun 0 /\ Dom 0 == A <-> A == 0) -> (isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> A == 0)
12 bian2 
Ran 0 C_ 0 -> (isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> isfun 0 /\ Dom 0 == A)
13 eqss 
Ran 0 == 0 -> Ran 0 C_ 0
14 rn0 
Ran 0 == 0
15 13, 14 ax_mp 
Ran 0 C_ 0
16 12, 15 ax_mp 
isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> isfun 0 /\ Dom 0 == A
17 11, 16 ax_mp 
(isfun 0 /\ Dom 0 == A <-> A == 0) -> (isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> A == 0)
18 bitr 
(isfun 0 /\ Dom 0 == A <-> Dom 0 == A) -> (Dom 0 == A <-> A == 0) -> (isfun 0 /\ Dom 0 == A <-> A == 0)
19 bian1 
isfun 0 -> (isfun 0 /\ Dom 0 == A <-> Dom 0 == A)
20 isf0 
isfun 0
21 19, 20 ax_mp 
isfun 0 /\ Dom 0 == A <-> Dom 0 == A
22 18, 21 ax_mp 
(Dom 0 == A <-> A == 0) -> (isfun 0 /\ Dom 0 == A <-> A == 0)
23 bitr 
(Dom 0 == A <-> 0 == A) -> (0 == A <-> A == 0) -> (Dom 0 == A <-> A == 0)
24 eqseq1 
Dom 0 == 0 -> (Dom 0 == A <-> 0 == A)
25 dm0 
Dom 0 == 0
26 24, 25 ax_mp 
Dom 0 == A <-> 0 == A
27 23, 26 ax_mp 
(0 == A <-> A == 0) -> (Dom 0 == A <-> A == 0)
28 eqscomb 
0 == A <-> A == 0
29 27, 28 ax_mp 
Dom 0 == A <-> A == 0
30 22, 29 ax_mp 
isfun 0 /\ Dom 0 == A <-> A == 0
31 17, 30 ax_mp 
isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0 <-> A == 0
32 funceq1 
F == 0 -> (func F A 0 <-> func 0 A 0)
33 32 conv func 
F == 0 -> (func F A 0 <-> isfun 0 /\ Dom 0 == A /\ Ran 0 C_ 0)
34 31, 33 syl6bb 
F == 0 -> (func F A 0 <-> A == 0)
35 10, 34 ax_mp 
F == 0 /\ func F A 0 <-> F == 0 /\ A == 0
36 9, 35 ax_mp 
func F A 0 <-> F == 0 /\ A == 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)