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