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 ∈ A B C → ∃ y y ∈ A B C ∧ 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 ∈ A B C , x = A → x = A
3 en3lplem1VD ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → ∃ y y ∈ A B C ∧ y ∈ x
4 1 2 3 e13 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C , x = A → ∃ y y ∈ A B C ∧ y ∈ x
5 4 in3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → x = A → ∃ y y ∈ A B C ∧ 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 ∈ A B C , x = B → x = B
9 en3lplem1VD ⊢ B ∈ C ∧ C ∈ A ∧ A ∈ B → x = B → ∃ y y ∈ B C A ∧ y ∈ x
10 7 8 9 e13 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C , x = B → ∃ y y ∈ B C A ∧ y ∈ x
11 tprot ⊢ A B C = B C A
12 11 eleq2i ⊢ y ∈ A B C ↔ y ∈ B C A
13 12 anbi1i ⊢ y ∈ A B C ∧ y ∈ x ↔ y ∈ B C A ∧ y ∈ x
14 13 exbii ⊢ ∃ y y ∈ A B C ∧ y ∈ x ↔ ∃ y y ∈ B C A ∧ y ∈ x
15 10 14 e3bir ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C , x = B → ∃ y y ∈ A B C ∧ y ∈ x
16 15 in3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → x = B → ∃ y y ∈ A B C ∧ y ∈ x
17 jao ⊢ x = A → ∃ y y ∈ A B C ∧ y ∈ x → x = B → ∃ y y ∈ A B C ∧ y ∈ x → x = A ∨ x = B → ∃ y y ∈ A B C ∧ y ∈ x
18 5 16 17 e22 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → x = A ∨ x = B → ∃ y y ∈ A B C ∧ 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 ∈ A B C , x = C → x = C
22 en3lplem1VD ⊢ C ∈ A ∧ A ∈ B ∧ B ∈ C → x = C → ∃ y y ∈ C A B ∧ y ∈ x
23 20 21 22 e13 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C , x = C → ∃ y y ∈ C A B ∧ y ∈ x
24 tprot ⊢ C A B = A B C
25 24 eleq2i ⊢ y ∈ C A B ↔ y ∈ A B C
26 25 anbi1i ⊢ y ∈ C A B ∧ y ∈ x ↔ y ∈ A B C ∧ y ∈ x
27 26 exbii ⊢ ∃ y y ∈ C A B ∧ y ∈ x ↔ ∃ y y ∈ A B C ∧ y ∈ x
28 23 27 e3bi ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C , x = C → ∃ y y ∈ A B C ∧ y ∈ x
29 28 in3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → x = C → ∃ y y ∈ A B C ∧ y ∈ x
30 idn2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → x ∈ A B C
31 dftp2 ⊢ A B C = x | x = A ∨ x = B ∨ x = C
32 31 eleq2i ⊢ x ∈ A B C ↔ x ∈ x | x = A ∨ x = B ∨ x = C
33 30 32 e2bi ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → 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 ∈ A B C → 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 ∈ A B C → x = A ∨ x = B ∨ x = C
38 jao ⊢ x = A ∨ x = B → ∃ y y ∈ A B C ∧ y ∈ x → x = C → ∃ y y ∈ A B C ∧ y ∈ x → x = A ∨ x = B ∨ x = C → ∃ y y ∈ A B C ∧ y ∈ x
39 18 29 37 38 e222 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x
40 39 in2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x
41 40 in1 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x