Theorem tpssad

Description: If an ordered triple is a subset of a class, the first element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	tpssad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	tpssad.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
Assertion	tpssad	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		tpssad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		tpssad.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
3	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → 𝐴 ∈ 𝑉 )
4		tpcomb	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 , 𝐵 }
5		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → ¬ 𝐵 ∈ V )
6	5	intnanrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → ¬ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐶 ) )
7		tpprceq3	⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐶 , 𝐵 } = { 𝐴 , 𝐶 } )
8	6 7	syl	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐶 , 𝐵 } = { 𝐴 , 𝐶 } )
9	4 8	eqtrid	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 } )
10	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
11	9 10	eqsstrrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐶 } ⊆ 𝐷 )
12	3 11	prssad	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → 𝐴 ∈ 𝐷 )
13	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → 𝐴 ∈ 𝑉 )
14		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ¬ 𝐶 ∈ V )
15	14	intnanrd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) )
16		tpprceq3	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
17	15 16	syl	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
18	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
19	17 18	eqsstrrd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 } ⊆ 𝐷 )
20	13 19	prssad	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → 𝐴 ∈ 𝐷 )
21	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ∈ 𝑉 )
22		simprl	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐵 ∈ V )
23		simprr	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐶 ∈ V )
24	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
25		tpssg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ↔ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 ) )
26	25	biimpar	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) )
27	21 22 23 24 26	syl31anc	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) )
28	27	simp1d	⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ∈ 𝐷 )
29	12 20 28	pm2.61dda	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )