Theorem sstrALT2VD

Description: Virtual deduction proof of sstrALT2 . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sstrALT2VD	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
2		idn1	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    )
3		simpr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
4	2 3	e1a	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    𝐵 ⊆ 𝐶    )
5		simpl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐵 )
6	2 5	e1a	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    𝐴 ⊆ 𝐵    )
7		idn2	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ,    𝑥 ∈ 𝐴    ▶    𝑥 ∈ 𝐴    )
8		ssel2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
9	6 7 8	e12an	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ,    𝑥 ∈ 𝐴    ▶    𝑥 ∈ 𝐵    )
10		ssel2	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 )
11	4 9 10	e12an	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ,    𝑥 ∈ 𝐴    ▶    𝑥 ∈ 𝐶    )
12	11	in2	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 )    )
13	12	gen11	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 )    )
14		biimpr	⊢ ( ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 ) )
15	1 13 14	e01	⊢ (    ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 )    ▶    𝐴 ⊆ 𝐶    )
16	15	in1	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )