Theorem ljoinT ≪ | index | src | ≫

theorem ljoinT (A: set) (L: nat): $ L e. List (List A) <-> ljoin L e. List A $;

Step	Hyp	Ref	Expression
1		id	_1 = L -> _1 = L
2	1	eleq1d	_1 = L -> (_1 e. List (List A) <-> L e. List (List A))
3	1	ljoineqd	_1 = L -> ljoin _1 = ljoin L
4	3	eleq1d	_1 = L -> (ljoin _1 e. List A <-> ljoin L e. List A)
5	2, 4	bieqd	_1 = L -> (_1 e. List (List A) <-> ljoin _1 e. List A <-> (L e. List (List A) <-> ljoin L e. List A))
6		id	_1 = 0 -> _1 = 0
7	6	eleq1d	_1 = 0 -> (_1 e. List (List A) <-> 0 e. List (List A))
8	6	ljoineqd	_1 = 0 -> ljoin _1 = ljoin 0
9	8	eleq1d	_1 = 0 -> (ljoin _1 e. List A <-> ljoin 0 e. List A)
10	7, 9	bieqd	_1 = 0 -> (_1 e. List (List A) <-> ljoin _1 e. List A <-> (0 e. List (List A) <-> ljoin 0 e. List A))
11		id	_1 = a2 -> _1 = a2
12	11	eleq1d	_1 = a2 -> (_1 e. List (List A) <-> a2 e. List (List A))
13	11	ljoineqd	_1 = a2 -> ljoin _1 = ljoin a2
14	13	eleq1d	_1 = a2 -> (ljoin _1 e. List A <-> ljoin a2 e. List A)
15	12, 14	bieqd	_1 = a2 -> (_1 e. List (List A) <-> ljoin _1 e. List A <-> (a2 e. List (List A) <-> ljoin a2 e. List A))
16		id	_1 = a1 : a2 -> _1 = a1 : a2
17	16	eleq1d	_1 = a1 : a2 -> (_1 e. List (List A) <-> a1 : a2 e. List (List A))
18	16	ljoineqd	_1 = a1 : a2 -> ljoin _1 = ljoin (a1 : a2)
19	18	eleq1d	_1 = a1 : a2 -> (ljoin _1 e. List A <-> ljoin (a1 : a2) e. List A)
20	17, 19	bieqd	_1 = a1 : a2 -> (_1 e. List (List A) <-> ljoin _1 e. List A <-> (a1 : a2 e. List (List A) <-> ljoin (a1 : a2) e. List A))
21		bith	0 e. List (List A) -> ljoin 0 e. List A -> (0 e. List (List A) <-> ljoin 0 e. List A)
22		elList0	0 e. List (List A)
23	21, 22	ax_mp	ljoin 0 e. List A -> (0 e. List (List A) <-> ljoin 0 e. List A)
24		eleq1	ljoin 0 = 0 -> (ljoin 0 e. List A <-> 0 e. List A)
25		ljoin0	ljoin 0 = 0
26	24, 25	ax_mp	ljoin 0 e. List A <-> 0 e. List A
27		elList0	0 e. List A
28	26, 27	mpbir	ljoin 0 e. List A
29	23, 28	ax_mp	0 e. List (List A) <-> ljoin 0 e. List A
30		elListS	a1 : a2 e. List (List A) <-> a1 e. List A /\ a2 e. List (List A)
31		eleq1	ljoin (a1 : a2) = a1 ++ ljoin a2 -> (ljoin (a1 : a2) e. List A <-> a1 ++ ljoin a2 e. List A)
32		ljoinS	ljoin (a1 : a2) = a1 ++ ljoin a2
33	31, 32	ax_mp	ljoin (a1 : a2) e. List A <-> a1 ++ ljoin a2 e. List A
34		appendT	a1 ++ ljoin a2 e. List A <-> a1 e. List A /\ ljoin a2 e. List A
35		id	(a2 e. List (List A) <-> ljoin a2 e. List A) -> (a2 e. List (List A) <-> ljoin a2 e. List A)
36	35	aneq2d	(a2 e. List (List A) <-> ljoin a2 e. List A) -> (a1 e. List A /\ a2 e. List (List A) <-> a1 e. List A /\ ljoin a2 e. List A)
37	34, 36	syl6bbr	(a2 e. List (List A) <-> ljoin a2 e. List A) -> (a1 e. List A /\ a2 e. List (List A) <-> a1 ++ ljoin a2 e. List A)
38	33, 37	syl6bbr	(a2 e. List (List A) <-> ljoin a2 e. List A) -> (a1 e. List A /\ a2 e. List (List A) <-> ljoin (a1 : a2) e. List A)
39	30, 38	syl5bb	(a2 e. List (List A) <-> ljoin a2 e. List A) -> (a1 : a2 e. List (List A) <-> ljoin (a1 : a2) e. List A)
40	5, 10, 15, 20, 29, 39	listind	L e. List (List A) <-> ljoin L 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)