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

Metamath Proof Explorer

Theorem en3lplem1VD

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

Ref Expression
Assertion en3lplem1VD ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    )
2 simp3 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ 𝐴 )
3 1 2 e1a ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    𝐶 ∈ 𝐴    )
4 tpid3g ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
5 3 4 e1a ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 }    )
6 idn2 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 = 𝐴    ▶    𝑥 = 𝐴    )
7 eleq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴 ) )
8 7 biimprd ⊢ ( 𝑥 = 𝐴 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝑥 ) )
9 6 3 8 e21 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 = 𝐴    ▶    𝐶 ∈ 𝑥    )
10 pm3.2 ⊢ ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝐶 ∈ 𝑥 → ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐶 ∈ 𝑥 ) ) )
11 5 9 10 e12 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 = 𝐴    ▶    ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐶 ∈ 𝑥 )    )
12 elex22 ⊢ ( ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐶 ∈ 𝑥 ) → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )
13 11 12 e2 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ,    𝑥 = 𝐴    ▶    ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 )    )
14 13 in2 ⊢ (    ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    ▶    ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )    )
15 14 in1 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )