# Metamath Proof Explorer

## Theorem en3lplem2VD

Description: Virtual deduction proof of en3lplem2 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en3lplem2VD ${⊢}\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)\to \left({x}\in \left\{{A},{B},{C}\right\}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 idn1 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){\to }\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)\right)$
2 idn3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={A}{\to }{x}={A}\right)$
3 en3lplem1VD ${⊢}\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)\to \left({x}={A}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$
4 1 2 3 e13 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={A}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$
5 4 in3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left({x}={A}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
6 3anrot ${⊢}\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)↔\left({B}\in {C}\wedge {C}\in {A}\wedge {A}\in {B}\right)$
7 1 6 e1bi ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){\to }\left({B}\in {C}\wedge {C}\in {A}\wedge {A}\in {B}\right)\right)$
8 idn3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={B}{\to }{x}={B}\right)$
9 en3lplem1VD ${⊢}\left({B}\in {C}\wedge {C}\in {A}\wedge {A}\in {B}\right)\to \left({x}={B}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{B},{C},{A}\right\}\wedge {y}\in {x}\right)\right)$
10 7 8 9 e13 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={B}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{B},{C},{A}\right\}\wedge {y}\in {x}\right)\right)$
11 tprot ${⊢}\left\{{A},{B},{C}\right\}=\left\{{B},{C},{A}\right\}$
12 11 eleq2i ${⊢}{y}\in \left\{{A},{B},{C}\right\}↔{y}\in \left\{{B},{C},{A}\right\}$
13 12 anbi1i ${⊢}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)↔\left({y}\in \left\{{B},{C},{A}\right\}\wedge {y}\in {x}\right)$
14 13 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{B},{C},{A}\right\}\wedge {y}\in {x}\right)$
15 10 14 e3bir ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={B}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$
16 15 in3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left({x}={B}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
17 jao ${⊢}\left({x}={A}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\to \left(\left({x}={B}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\to \left(\left({x}={A}\vee {x}={B}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
18 5 16 17 e22 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left(\left({x}={A}\vee {x}={B}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
19 3anrot ${⊢}\left({C}\in {A}\wedge {A}\in {B}\wedge {B}\in {C}\right)↔\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)$
20 1 19 e1bir ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){\to }\left({C}\in {A}\wedge {A}\in {B}\wedge {B}\in {C}\right)\right)$
21 idn3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={C}{\to }{x}={C}\right)$
22 en3lplem1VD ${⊢}\left({C}\in {A}\wedge {A}\in {B}\wedge {B}\in {C}\right)\to \left({x}={C}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{C},{A},{B}\right\}\wedge {y}\in {x}\right)\right)$
23 20 21 22 e13 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={C}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{C},{A},{B}\right\}\wedge {y}\in {x}\right)\right)$
24 tprot ${⊢}\left\{{C},{A},{B}\right\}=\left\{{A},{B},{C}\right\}$
25 24 eleq2i ${⊢}{y}\in \left\{{C},{A},{B}\right\}↔{y}\in \left\{{A},{B},{C}\right\}$
26 25 anbi1i ${⊢}\left({y}\in \left\{{C},{A},{B}\right\}\wedge {y}\in {x}\right)↔\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)$
27 26 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{C},{A},{B}\right\}\wedge {y}\in {x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)$
28 23 27 e3bi ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{,}{x}={C}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$
29 28 in3 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left({x}={C}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
30 idn2 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }{x}\in \left\{{A},{B},{C}\right\}\right)$
31 dftp2 ${⊢}\left\{{A},{B},{C}\right\}=\left\{{x}|\left({x}={A}\vee {x}={B}\vee {x}={C}\right)\right\}$
32 31 eleq2i ${⊢}{x}\in \left\{{A},{B},{C}\right\}↔{x}\in \left\{{x}|\left({x}={A}\vee {x}={B}\vee {x}={C}\right)\right\}$
33 30 32 e2bi ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }{x}\in \left\{{x}|\left({x}={A}\vee {x}={B}\vee {x}={C}\right)\right\}\right)$
34 abid ${⊢}{x}\in \left\{{x}|\left({x}={A}\vee {x}={B}\vee {x}={C}\right)\right\}↔\left({x}={A}\vee {x}={B}\vee {x}={C}\right)$
35 33 34 e2bi ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left({x}={A}\vee {x}={B}\vee {x}={C}\right)\right)$
36 df-3or ${⊢}\left({x}={A}\vee {x}={B}\vee {x}={C}\right)↔\left(\left({x}={A}\vee {x}={B}\right)\vee {x}={C}\right)$
37 35 36 e2bi ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\left(\left({x}={A}\vee {x}={B}\right)\vee {x}={C}\right)\right)$
38 jao ${⊢}\left(\left({x}={A}\vee {x}={B}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\to \left(\left({x}={C}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\to \left(\left(\left({x}={A}\vee {x}={B}\right)\vee {x}={C}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
39 18 29 37 38 e222 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){,}{x}\in \left\{{A},{B},{C}\right\}{\to }\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$
40 39 in2 ${⊢}\left(\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right){\to }\left({x}\in \left\{{A},{B},{C}\right\}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)\right)$
41 40 in1 ${⊢}\left({A}\in {B}\wedge {B}\in {C}\wedge {C}\in {A}\right)\to \left({x}\in \left\{{A},{B},{C}\right\}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{A},{B},{C}\right\}\wedge {y}\in {x}\right)\right)$