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	|- ( ph -> A e. V )
	tpssad.2	|- ( ph -> { A , B , C } C_ D )
Assertion	tpssad	|- ( ph -> A e. D )

Proof

Step	Hyp	Ref	Expression
1		tpssad.1	|- ( ph -> A e. V )
2		tpssad.2	|- ( ph -> { A , B , C } C_ D )
3	1	adantr	|- ( ( ph /\ -. B e. _V ) -> A e. V )
4		tpcomb	|- { A , B , C } = { A , C , B }
5		simpr	|- ( ( ph /\ -. B e. _V ) -> -. B e. _V )
6	5	intnanrd	|- ( ( ph /\ -. B e. _V ) -> -. ( B e. _V /\ B =/= C ) )
7		tpprceq3	|- ( -. ( B e. _V /\ B =/= C ) -> { A , C , B } = { A , C } )
8	6 7	syl	|- ( ( ph /\ -. B e. _V ) -> { A , C , B } = { A , C } )
9	4 8	eqtrid	|- ( ( ph /\ -. B e. _V ) -> { A , B , C } = { A , C } )
10	2	adantr	|- ( ( ph /\ -. B e. _V ) -> { A , B , C } C_ D )
11	9 10	eqsstrrd	|- ( ( ph /\ -. B e. _V ) -> { A , C } C_ D )
12	3 11	prssad	|- ( ( ph /\ -. B e. _V ) -> A e. D )
13	1	adantr	|- ( ( ph /\ -. C e. _V ) -> A e. V )
14		simpr	|- ( ( ph /\ -. C e. _V ) -> -. C e. _V )
15	14	intnanrd	|- ( ( ph /\ -. C e. _V ) -> -. ( C e. _V /\ C =/= B ) )
16		tpprceq3	|- ( -. ( C e. _V /\ C =/= B ) -> { A , B , C } = { A , B } )
17	15 16	syl	|- ( ( ph /\ -. C e. _V ) -> { A , B , C } = { A , B } )
18	2	adantr	|- ( ( ph /\ -. C e. _V ) -> { A , B , C } C_ D )
19	17 18	eqsstrrd	|- ( ( ph /\ -. C e. _V ) -> { A , B } C_ D )
20	13 19	prssad	|- ( ( ph /\ -. C e. _V ) -> A e. D )
21	1	adantr	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> A e. V )
22		simprl	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> B e. _V )
23		simprr	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> C e. _V )
24	2	adantr	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> { A , B , C } C_ D )
25		tpssg	|- ( ( A e. V /\ B e. _V /\ C e. _V ) -> ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D ) )
26	25	biimpar	|- ( ( ( A e. V /\ B e. _V /\ C e. _V ) /\ { A , B , C } C_ D ) -> ( A e. D /\ B e. D /\ C e. D ) )
27	21 22 23 24 26	syl31anc	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> ( A e. D /\ B e. D /\ C e. D ) )
28	27	simp1d	|- ( ( ph /\ ( B e. _V /\ C e. _V ) ) -> A e. D )
29	12 20 28	pm2.61dda	|- ( ph -> A e. D )