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 ⊢A∈B∧B∈C∧C∈A→x∈ABC→∃yy∈ABC∧y∈x

Proof

Step Hyp Ref Expression
1 idn1 ⊢A∈B∧B∈C∧C∈A→A∈B∧B∈C∧C∈A
2 idn3 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=A→x=A
3 en3lplem1VD ⊢A∈B∧B∈C∧C∈A→x=A→∃yy∈ABC∧y∈x
4 1 2 3 e13 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=A→∃yy∈ABC∧y∈x
5 4 in3 ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=A→∃yy∈ABC∧y∈x
6 3anrot ⊢A∈B∧B∈C∧C∈A↔B∈C∧C∈A∧A∈B
7 1 6 e1bi ⊢A∈B∧B∈C∧C∈A→B∈C∧C∈A∧A∈B
8 idn3 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=B→x=B
9 en3lplem1VD ⊢B∈C∧C∈A∧A∈B→x=B→∃yy∈BCA∧y∈x
10 7 8 9 e13 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=B→∃yy∈BCA∧y∈x
11 tprot ⊢ABC=BCA
12 11 eleq2i ⊢y∈ABC↔y∈BCA
13 12 anbi1i ⊢y∈ABC∧y∈x↔y∈BCA∧y∈x
14 13 exbii ⊢∃yy∈ABC∧y∈x↔∃yy∈BCA∧y∈x
15 10 14 e3bir ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=B→∃yy∈ABC∧y∈x
16 15 in3 ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=B→∃yy∈ABC∧y∈x
17 jao ⊢x=A→∃yy∈ABC∧y∈x→x=B→∃yy∈ABC∧y∈x→x=A∨x=B→∃yy∈ABC∧y∈x
18 5 16 17 e22 ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=A∨x=B→∃yy∈ABC∧y∈x
19 3anrot ⊢C∈A∧A∈B∧B∈C↔A∈B∧B∈C∧C∈A
20 1 19 e1bir ⊢A∈B∧B∈C∧C∈A→C∈A∧A∈B∧B∈C
21 idn3 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=C→x=C
22 en3lplem1VD ⊢C∈A∧A∈B∧B∈C→x=C→∃yy∈CAB∧y∈x
23 20 21 22 e13 ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=C→∃yy∈CAB∧y∈x
24 tprot ⊢CAB=ABC
25 24 eleq2i ⊢y∈CAB↔y∈ABC
26 25 anbi1i ⊢y∈CAB∧y∈x↔y∈ABC∧y∈x
27 26 exbii ⊢∃yy∈CAB∧y∈x↔∃yy∈ABC∧y∈x
28 23 27 e3bi ⊢A∈B∧B∈C∧C∈A,x∈ABC,x=C→∃yy∈ABC∧y∈x
29 28 in3 ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=C→∃yy∈ABC∧y∈x
30 idn2 ⊢A∈B∧B∈C∧C∈A,x∈ABC→x∈ABC
31 dftp2 ⊢ABC=x|x=A∨x=B∨x=C
32 31 eleq2i ⊢x∈ABC↔x∈x|x=A∨x=B∨x=C
33 30 32 e2bi ⊢A∈B∧B∈C∧C∈A,x∈ABC→x∈x|x=A∨x=B∨x=C
34 abid ⊢x∈x|x=A∨x=B∨x=C↔x=A∨x=B∨x=C
35 33 34 e2bi ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=A∨x=B∨x=C
36 df-3or ⊢x=A∨x=B∨x=C↔x=A∨x=B∨x=C
37 35 36 e2bi ⊢A∈B∧B∈C∧C∈A,x∈ABC→x=A∨x=B∨x=C
38 jao ⊢x=A∨x=B→∃yy∈ABC∧y∈x→x=C→∃yy∈ABC∧y∈x→x=A∨x=B∨x=C→∃yy∈ABC∧y∈x
39 18 29 37 38 e222 ⊢A∈B∧B∈C∧C∈A,x∈ABC→∃yy∈ABC∧y∈x
40 39 in2 ⊢A∈B∧B∈C∧C∈A→x∈ABC→∃yy∈ABC∧y∈x
41 40 in1 ⊢A∈B∧B∈C∧C∈A→x∈ABC→∃yy∈ABC∧y∈x