This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. ( A e. B /\ B e. C /\ C e. A ) ).
2 idn3 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x e. { A , B , C } ,. x = A ->. x = A ).
3 en3lplem1VD 
 |-  ( ( 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 
 |-  (. ( 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 
 |-  (. ( 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 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) <-> ( B e. C /\ C e. A /\ A e. B ) )
7 1 6 e1bi 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. ( B e. C /\ C e. A /\ A e. B ) ).
8 idn3 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x e. { A , B , C } ,. x = B ->. x = B ).
9 en3lplem1VD 
 |-  ( ( 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 
 |-  (. ( 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 
 |-  { A , B , C } = { B , C , A }
12 11 eleq2i 
 |-  ( y e. { A , B , C } <-> y e. { B , C , A } )
13 12 anbi1i 
 |-  ( ( y e. { A , B , C } /\ y e. x ) <-> ( y e. { B , C , A } /\ y e. x ) )
14 13 exbii 
 |-  ( E. y ( y e. { A , B , C } /\ y e. x ) <-> E. y ( y e. { B , C , A } /\ y e. x ) )
15 10 14 e3bir 
 |-  (. ( 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 
 |-  (. ( 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 
 |-  ( ( 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 
 |-  (. ( 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 
 |-  ( ( C e. A /\ A e. B /\ B e. C ) <-> ( A e. B /\ B e. C /\ C e. A ) )
20 1 19 e1bir 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. ( C e. A /\ A e. B /\ B e. C ) ).
21 idn3 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x e. { A , B , C } ,. x = C ->. x = C ).
22 en3lplem1VD 
 |-  ( ( 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 
 |-  (. ( 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 
 |-  { C , A , B } = { A , B , C }
25 24 eleq2i 
 |-  ( y e. { C , A , B } <-> y e. { A , B , C } )
26 25 anbi1i 
 |-  ( ( y e. { C , A , B } /\ y e. x ) <-> ( y e. { A , B , C } /\ y e. x ) )
27 26 exbii 
 |-  ( E. y ( y e. { C , A , B } /\ y e. x ) <-> E. y ( y e. { A , B , C } /\ y e. x ) )
28 23 27 e3bi 
 |-  (. ( 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 
 |-  (. ( 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 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x e. { A , B , C } ->. x e. { A , B , C } ).
31 dftp2 
 |-  { A , B , C } = { x | ( x = A \/ x = B \/ x = C ) }
32 31 eleq2i 
 |-  ( x e. { A , B , C } <-> x e. { x | ( x = A \/ x = B \/ x = C ) } )
33 30 32 e2bi 
 |-  (. ( 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 
 |-  ( x e. { x | ( x = A \/ x = B \/ x = C ) } <-> ( x = A \/ x = B \/ x = C ) )
35 33 34 e2bi 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x e. { 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 e. B /\ B e. C /\ C e. A ) ,. x e. { A , B , C } ->. ( ( x = A \/ x = B ) \/ x = C ) ).
38 jao 
 |-  ( ( ( 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 
 |-  (. ( 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 
 |-  (. ( 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 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x e. { A , B , C } -> E. y ( y e. { A , B , C } /\ y e. x ) ) )