Theorem en3lplem2VD 16668

Description: Virtual deduction proof of en3lplem2 5757.

Assertion

Ref	Expression
en3lplem2VD	|- ((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 en3lplem2VD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . . 7 |- . (A e. B /\ B e. C /\ C e. A)   ⊢   (A e. B /\ B e. C /\ C e. A) .
2		idn3 16510	. . . . . . 7 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}, x = A   ⊢   x = A .
3		en3lplem1 5756	. . . . . . 7 |- ((A e. B /\ B e. C /\ C e. A) -> (x = A -> E.y(y e. {A, B, C} /\ y e. x)))
4	1, 2, 3	e13 16616	. . . . . 6 |- . (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) .
5	4	in3 16508	. . . . 5 |- . (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)) .
6		3anrot 863	. . . . . . . . 9 |- ((A e. B /\ B e. C /\ C e. A) <-> (B e. C /\ C e. A /\ A e. B))
7	1, 6	e1bi 16519	. . . . . . . 8 |- . (A e. B /\ B e. C /\ C e. A)   ⊢   (B e. C /\ C e. A /\ A e. B) .
8		idn3 16510	. . . . . . . 8 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}, x = B   ⊢   x = B .
9		en3lplem1 5756	. . . . . . . 8 |- ((B e. C /\ C e. A /\ A e. B) -> (x = B -> E.y(y e. {B, C, A} /\ y e. x)))
10	7, 8, 9	e13 16616	. . . . . . 7 |- . (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) .
11		tprot 3103	. . . . . . . . . 10 |- {A, B, C} = {B, C, A}
12	11	eleq2i 1961	. . . . . . . . 9 |- (y e. {A, B, C} <-> y e. {B, C, A})
13	12	anbi1i 539	. . . . . . . 8 |- ((y e. {A, B, C} /\ y e. x) <-> (y e. {B, C, A} /\ y e. x))
14	13	exbii 1398	. . . . . . 7 |- (E.y(y e. {A, B, C} /\ y e. x) <-> E.y(y e. {B, C, A} /\ y e. x))
15	10, 14	e3bir 16607	. . . . . 6 |- . (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) .
16	15	in3 16508	. . . . 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)) .
17		jao 367	. . . . 5 |- ((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))))
18	5, 16, 17	e22 16561	. . . 4 |- . (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)) .
19		3anrot 863	. . . . . . . 8 |- ((C e. A /\ A e. B /\ B e. C) <-> (A e. B /\ B e. C /\ C e. A))
20	1, 19	e1bir 16520	. . . . . . 7 |- . (A e. B /\ B e. C /\ C e. A)   ⊢   (C e. A /\ A e. B /\ B e. C) .
21		idn3 16510	. . . . . . 7 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}, x = C   ⊢   x = C .
22		en3lplem1 5756	. . . . . . 7 |- ((C e. A /\ A e. B /\ B e. C) -> (x = C -> E.y(y e. {C, A, B} /\ y e. x)))
23	20, 21, 22	e13 16616	. . . . . 6 |- . (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) .
24		tprot 3103	. . . . . . . . 9 |- {C, A, B} = {A, B, C}
25	24	eleq2i 1961	. . . . . . . 8 |- (y e. {C, A, B} <-> y e. {A, B, C})
26	25	anbi1i 539	. . . . . . 7 |- ((y e. {C, A, B} /\ y e. x) <-> (y e. {A, B, C} /\ y e. x))
27	26	exbii 1398	. . . . . 6 |- (E.y(y e. {C, A, B} /\ y e. x) <-> E.y(y e. {A, B, C} /\ y e. x))
28	23, 27	e3bi 16606	. . . . 5 |- . (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) .
29	28	in3 16508	. . . 4 |- . (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)) .
30		idn2 16509	. . . . . . 7 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}   ⊢   x e. {A, B, C} .
31		dftp2 3075	. . . . . . . 8 |- {A, B, C} = {x | (x = A \/ x = B \/ x = C)}
32	31	eleq2i 1961	. . . . . . 7 |- (x e. {A, B, C} <-> x e. {x | (x = A \/ x = B \/ x = C)})
33	30, 32	e2bi 16522	. . . . . 6 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}   ⊢   x e. {x | (x = A \/ x = B \/ x = C)} .
34		abid 1873	. . . . . 6 |- (x e. {x | (x = A \/ x = B \/ x = C)} <-> (x = A \/ x = B \/ x = C))
35	33, 34	e2bi 16522	. . . . 5 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}   ⊢   (x = A \/ x = B \/ x = C) .
36		df-3or 859	. . . . 5 |- ((x = A \/ x = B \/ x = C) <-> ((x = A \/ x = B) \/ x = C))
37	35, 36	e2bi 16522	. . . 4 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}   ⊢   ((x = A \/ x = B) \/ x = C) .
38		jao 367	. . . 4 |- (((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))))
39	18, 29, 37, 38	e222 16526	. . 3 |- . (A e. B /\ B e. C /\ C e. A), x e. {A, B, C}   ⊢   E.y(y e. {A, B, C} /\ y e. x) .
40	39	in2 16506	. 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)) .
41	40	in1 16481	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 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  df-vd1 16480  df-vd2 16489  df-vd3 16494

Copyright terms: Public domain