Theorem reseq0 ≪ | index | src | ≫ 

theorem reseq0 (A F: set): $ Dom F i^i A == 0 <-> F |` A == 0 $;
StepHypRefExpression
1 bitr4 
(Dom F i^i A == 0 <-> Dom F C_ Compl A) -> (F |` A == 0 <-> Dom F C_ Compl A) -> (Dom F i^i A == 0 <-> F |` A == 0)
2 ineq0 
Dom F i^i A == 0 <-> Dom F C_ Compl A
3 1, 2 ax_mp 
(F |` A == 0 <-> Dom F C_ Compl A) -> (Dom F i^i A == 0 <-> F |` A == 0)
4 bitr4 
(F |` A == 0 <-> F C_ Compl (Xp A _V)) -> (Dom F C_ Compl A <-> F C_ Compl (Xp A _V)) -> (F |` A == 0 <-> Dom F C_ Compl A)
5 ineq0 
F i^i Xp A _V == 0 <-> F C_ Compl (Xp A _V)
6 5 conv res 
F |` A == 0 <-> F C_ Compl (Xp A _V)
7 4, 6 ax_mp 
(Dom F C_ Compl A <-> F C_ Compl (Xp A _V)) -> (F |` A == 0 <-> Dom F C_ Compl A)
8 bitr4 
(Dom F C_ Compl A <-> F C_ Xp (Compl A) _V) -> (F C_ Compl (Xp A _V) <-> F C_ Xp (Compl A) _V) -> (Dom F C_ Compl A <-> F C_ Compl (Xp A _V))
9 ssdm 
Dom F C_ Compl A <-> F C_ Xp (Compl A) _V
10 8, 9 ax_mp 
(F C_ Compl (Xp A _V) <-> F C_ Xp (Compl A) _V) -> (Dom F C_ Compl A <-> F C_ Compl (Xp A _V))
11 sseq2 
Compl (Xp A _V) == Xp (Compl A) _V -> (F C_ Compl (Xp A _V) <-> F C_ Xp (Compl A) _V)
12 cplxpv2 
Compl (Xp A _V) == Xp (Compl A) _V
13 11, 12 ax_mp 
F C_ Compl (Xp A _V) <-> F C_ Xp (Compl A) _V
14 10, 13 ax_mp 
Dom F C_ Compl A <-> F C_ Compl (Xp A _V)
15 7, 14 ax_mp 
F |` A == 0 <-> Dom F C_ Compl A
16 3, 15 ax_mp 
Dom F i^i A == 0 <-> F |` 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)