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 ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    )
2 idn3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐴    ▶    𝑥 = 𝐴    )
3 en3lplem1VD ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )
4 1 2 3 e13 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐴    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 )    )
5 4 in3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
6 3anrot ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ↔ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) )
7 1 6 e1bi ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 )    )
8 idn3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐵    ▶    𝑥 = 𝐵    )
9 en3lplem1VD ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 = 𝐵 → ∃ 𝑦 ( 𝑦 ∈ { 𝐵 , 𝐶 , 𝐴 } ∧ 𝑦 ∈ 𝑥 ) ) )
10 7 8 9 e13 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐵    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐵 , 𝐶 , 𝐴 } ∧ 𝑦 ∈ 𝑥 )    )
11 tprot ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
12 11 eleq2i ⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑦 ∈ { 𝐵 , 𝐶 , 𝐴 } )
13 12 anbi1i ⊢ ( ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ { 𝐵 , 𝐶 , 𝐴 } ∧ 𝑦 ∈ 𝑥 ) )
14 13 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝐵 , 𝐶 , 𝐴 } ∧ 𝑦 ∈ 𝑥 ) )
15 10 14 e3bir ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐵    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 )    )
16 15 in3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( 𝑥 = 𝐵 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
17 jao ⊢ ( ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑥 = 𝐵 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) ) )
18 5 16 17 e22 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
19 3anrot ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
20 1 19 e1bir ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 )    )
21 idn3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐶    ▶    𝑥 = 𝐶    )
22 en3lplem1VD ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ( 𝑥 = 𝐶 → ∃ 𝑦 ( 𝑦 ∈ { 𝐶 , 𝐴 , 𝐵 } ∧ 𝑦 ∈ 𝑥 ) ) )
23 20 21 22 e13 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐶    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐶 , 𝐴 , 𝐵 } ∧ 𝑦 ∈ 𝑥 )    )
24 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
25 24 eleq2i ⊢ ( 𝑦 ∈ { 𝐶 , 𝐴 , 𝐵 } ↔ 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } )
26 25 anbi1i ⊢ ( ( 𝑦 ∈ { 𝐶 , 𝐴 , 𝐵 } ∧ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )
27 26 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐶 , 𝐴 , 𝐵 } ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )
28 23 27 e3bi ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ,    𝑥 = 𝐶    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 )    )
29 28 in3 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( 𝑥 = 𝐶 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
30 idn2 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    )
31 dftp2 ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) }
32 31 eleq2i ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } )
33 30 32 e2bi ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) }    )
34 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
35 33 34 e2bi ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 )    )
36 df-3or ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) ↔ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) )
37 35 36 e2bi ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 )    )
38 jao ⊢ ( ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑥 = 𝐶 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) → ( ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∨ 𝑥 = 𝐶 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) ) )
39 18 29 37 38 e222 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 }    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 )    )
40 39 in2 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
41 40 in1 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )