Theorem sublistAtT ≪ | index | src | ≫ 

theorem sublistAtT (A: set) (L1 L2 n: nat):
  $ sublistAt n L1 L2 -> L1 e. List A -> L2 e. List A $;
StepHypRefExpression
1 appendT 
L2 ++ a2 e. List A <-> L2 e. List A /\ a2 e. List A
2 appendT 
a1 ++ L2 ++ a2 e. List A <-> a1 e. List A /\ L2 ++ a2 e. List A
3 anll 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> L1 = a1 ++ L2 ++ a2
4 3 eleq1d 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> (L1 e. List A <-> a1 ++ L2 ++ a2 e. List A)
5 anr 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> L1 e. List A
6 4, 5 mpbid 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> a1 ++ L2 ++ a2 e. List A
7 2, 6 sylib 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> a1 e. List A /\ L2 ++ a2 e. List A
8 7 anrd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> L2 ++ a2 e. List A
9 1, 8 sylib 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> L2 e. List A /\ a2 e. List A
10 9 anld 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ L1 e. List A -> L2 e. List A
11 10 exp 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> L1 e. List A -> L2 e. List A
12 11 eex 
E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> L1 e. List A -> L2 e. List A
13 12 eex 
E. a1 E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> L1 e. List A -> L2 e. List A
14 13 conv sublistAt 
sublistAt n L1 L2 -> L1 e. List A -> L2 e. List 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)