Theorem en3lplem2 5757

Description: Lemma for en3lp 5758. This proof was automatically generated from the virtual deduction proof en3lplem2VD 16668 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)

Assertion

Ref	Expression
en3lplem2	|- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> E.y(y e. {A, B, C} /\ y e. x)))

Distinct variable groups:   x,y,A   x,B,y   x,C,y

Proof of Theorem en3lplem2

Step	Hyp	Ref	Expression
1		id 73	. 2 |- ((A e. B /\ B e. C /\ C e. A) -> (A e. B /\ B e. C /\ C e. A))
2		en3lplem1 5756	. . . . 5 |- ((A e. B /\ B e. C /\ C e. A) -> (x = A -> E.y(y e. {A, B, C} /\ y e. x)))
3	2	a1d 15	. . . 4 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = A -> E.y(y e. {A, B, C} /\ y e. x))))
4		3anrot 863	. . . . . . . 8 |- ((A e. B /\ B e. C /\ C e. A) <-> (B e. C /\ C e. A /\ A e. B))
5	4	biimpi 168	. . . . . . 7 |- ((A e. B /\ B e. C /\ C e. A) -> (B e. C /\ C e. A /\ A e. B))
6		iidn3 1270	. . . . . . 7 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = B -> x = B)))
7		en3lplem1 5756	. . . . . . 7 |- ((B e. C /\ C e. A /\ A e. B) -> (x = B -> E.y(y e. {B, C, A} /\ y e. x)))
8	5, 6, 7	ee13 1275	. . . . . 6 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = B -> E.y(y e. {B, C, A} /\ y e. x))))
9		tprot 3103	. . . . . . . . 9 |- {A, B, C} = {B, C, A}
10	9	eleq2i 1961	. . . . . . . 8 |- (y e. {A, B, C} <-> y e. {B, C, A})
11	10	anbi1i 539	. . . . . . 7 |- ((y e. {A, B, C} /\ y e. x) <-> (y e. {B, C, A} /\ y e. x))
12	11	exbii 1398	. . . . . 6 |- (E.y(y e. {A, B, C} /\ y e. x) <-> E.y(y e. {B, C, A} /\ y e. x))
13	8, 12	ee3bir 1274	. . . . 5 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = B -> E.y(y e. {A, B, C} /\ y e. x))))
14	13	iin3 1269	. . . 4 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = B -> E.y(y e. {A, B, C} /\ y e. x))))
15		jao 367	. . . 4 |- ((x = A -> E.y(y e. {A, B, C} /\ y e. x)) -> ((x = B -> E.y(y e. {A, B, C} /\ y e. x)) -> ((x = A \/ x = B) -> E.y(y e. {A, B, C} /\ y e. x))))
16	3, 14, 15	ee22 1272	. . 3 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> ((x = A \/ x = B) -> E.y(y e. {A, B, C} /\ y e. x))))
17		3anrot 863	. . . . . 6 |- ((C e. A /\ A e. B /\ B e. C) <-> (A e. B /\ B e. C /\ C e. A))
18	17	biimpri 169	. . . . 5 |- ((A e. B /\ B e. C /\ C e. A) -> (C e. A /\ A e. B /\ B e. C))
19		iidn3 1270	. . . . 5 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = C -> x = C)))
20		en3lplem1 5756	. . . . 5 |- ((C e. A /\ A e. B /\ B e. C) -> (x = C -> E.y(y e. {C, A, B} /\ y e. x)))
21	18, 19, 20	ee13 1275	. . . 4 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = C -> E.y(y e. {C, A, B} /\ y e. x))))
22		tprot 3103	. . . . . . 7 |- {C, A, B} = {A, B, C}
23	22	eleq2i 1961	. . . . . 6 |- (y e. {C, A, B} <-> y e. {A, B, C})
24	23	anbi1i 539	. . . . 5 |- ((y e. {C, A, B} /\ y e. x) <-> (y e. {A, B, C} /\ y e. x))
25	24	exbii 1398	. . . 4 |- (E.y(y e. {C, A, B} /\ y e. x) <-> E.y(y e. {A, B, C} /\ y e. x))
26	21, 25	syl8ib 234	. . 3 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = C -> E.y(y e. {A, B, C} /\ y e. x))))
27		idd 75	. . . . . 6 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> x e. {A, B, C}))
28		dftp2 3075	. . . . . . 7 |- {A, B, C} = {x | (x = A \/ x = B \/ x = C)}
29	28	eleq2i 1961	. . . . . 6 |- (x e. {A, B, C} <-> x e. {x | (x = A \/ x = B \/ x = C)})
30	27, 29	syl6ib 229	. . . . 5 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> x e. {x | (x = A \/ x = B \/ x = C)}))
31		abid 1873	. . . . 5 |- (x e. {x | (x = A \/ x = B \/ x = C)} <-> (x = A \/ x = B \/ x = C))
32	30, 31	syl6ib 229	. . . 4 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> (x = A \/ x = B \/ x = C)))
33		df-3or 859	. . . 4 |- ((x = A \/ x = B \/ x = C) <-> ((x = A \/ x = B) \/ x = C))
34	32, 33	syl6ib 229	. . 3 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> ((x = A \/ x = B) \/ x = C)))
35		jao 367	. . 3 |- (((x = A \/ x = B) -> E.y(y e. {A, B, C} /\ y e. x)) -> ((x = C -> E.y(y e. {A, B, C} /\ y e. x)) -> (((x = A \/ x = B) \/ x = C) -> E.y(y e. {A, B, C} /\ y e. x))))
36	16, 26, 34, 35	ee222 1271	. 2 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> E.y(y e. {A, B, C} /\ y e. x)))
37	1, 36	syl 12	1 |- ((A e. B /\ B e. C /\ C e. A) -> (x e. {A, B, C} -> E.y(y e. {A, B, C} /\ y e. x)))

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  {ctp 3051

This theorem is referenced by:  en3lp 5758  en3lpVD 16669

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-tp 3052

Copyright terms: Public domain