Theorem ssrn ≪ | index | src | ≫ 

theorem ssrn (A R: set): $ Ran R C_ A <-> R C_ Xp _V A $;
StepHypRefExpression
1 bitr4 
(Ran R C_ A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (R C_ Xp _V A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (Ran R C_ A <-> R C_ Xp _V A)
2 bitr 
(a2 e. Ran R -> a2 e. A <-> E. a1 a1, a2 e. R -> a2 e. A) ->
  (E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (a2 e. Ran R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
3 elrn 
a2 e. Ran R <-> E. a1 a1, a2 e. R
4 3 imeq1i 
a2 e. Ran R -> a2 e. A <-> E. a1 a1, a2 e. R -> a2 e. A
5 2, 4 ax_mp 
(E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) -> (a2 e. Ran R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
6 bitr4 
(E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a2 e. A)) ->
  (A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a1 (a1, a2 e. R -> a2 e. A)) ->
  (E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
7 eexb 
E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a2 e. A)
8 6, 7 ax_mp 
(A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a1 (a1, a2 e. R -> a2 e. A)) -> (E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
9 bitr 
(a1, a2 e. Xp _V A <-> a1 e. _V /\ a2 e. A) -> (a1 e. _V /\ a2 e. A <-> a2 e. A) -> (a1, a2 e. Xp _V A <-> a2 e. A)
10 prelxp 
a1, a2 e. Xp _V A <-> a1 e. _V /\ a2 e. A
11 9, 10 ax_mp 
(a1 e. _V /\ a2 e. A <-> a2 e. A) -> (a1, a2 e. Xp _V A <-> a2 e. A)
12 bian1 
a1 e. _V -> (a1 e. _V /\ a2 e. A <-> a2 e. A)
13 elv 
a1 e. _V
14 12, 13 ax_mp 
a1 e. _V /\ a2 e. A <-> a2 e. A
15 11, 14 ax_mp 
a1, a2 e. Xp _V A <-> a2 e. A
16 15 imeq2i 
a1, a2 e. R -> a1, a2 e. Xp _V A <-> a1, a2 e. R -> a2 e. A
17 16 aleqi 
A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a1 (a1, a2 e. R -> a2 e. A)
18 8, 17 ax_mp 
E. a1 a1, a2 e. R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
19 5, 18 ax_mp 
a2 e. Ran R -> a2 e. A <-> A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
20 19 aleqi 
A. a2 (a2 e. Ran R -> a2 e. A) <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
21 20 conv subset 
Ran R C_ A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
22 1, 21 ax_mp 
(R C_ Xp _V A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) -> (Ran R C_ A <-> R C_ Xp _V A)
23 bitr 
(R C_ Xp _V A <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (R C_ Xp _V A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
24 ssal2 
R C_ Xp _V A <-> A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp _V A)
25 23, 24 ax_mp 
(A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)) ->
  (R C_ Xp _V A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A))
26 alcomb 
A. a1 A. a2 (a1, a2 e. R -> a1, a2 e. Xp _V A) <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
27 25, 26 ax_mp 
R C_ Xp _V A <-> A. a2 A. a1 (a1, a2 e. R -> a1, a2 e. Xp _V A)
28 22, 27 ax_mp 
Ran R C_ A <-> R C_ Xp _V A

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)