Metamath Proof Explorer

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 ⊢ φ → A ∈ V
tpssad.2 ⊢ φ → A B C ⊆ D
Assertion tpssad ⊢ φ → A ∈ D

Proof

Step Hyp Ref Expression
1 tpssad.1 ⊢ φ → A ∈ V
2 tpssad.2 ⊢ φ → A B C ⊆ D
3 1 adantr ⊢ φ ∧ ¬ B ∈ V → A ∈ V
4 tpcomb ⊢ A B C = A C B
5 simpr ⊢ φ ∧ ¬ B ∈ V → ¬ B ∈ V
6 5 intnanrd ⊢ φ ∧ ¬ B ∈ V → ¬ B ∈ V ∧ B ≠ C
7 tpprceq3 ⊢ ¬ B ∈ V ∧ B ≠ C → A C B = A C
8 6 7 syl ⊢ φ ∧ ¬ B ∈ V → A C B = A C
9 4 8 eqtrid ⊢ φ ∧ ¬ B ∈ V → A B C = A C
10 2 adantr ⊢ φ ∧ ¬ B ∈ V → A B C ⊆ D
11 9 10 eqsstrrd ⊢ φ ∧ ¬ B ∈ V → A C ⊆ D
12 3 11 prssad ⊢ φ ∧ ¬ B ∈ V → A ∈ D
13 1 adantr ⊢ φ ∧ ¬ C ∈ V → A ∈ V
14 simpr ⊢ φ ∧ ¬ C ∈ V → ¬ C ∈ V
15 14 intnanrd ⊢ φ ∧ ¬ C ∈ V → ¬ C ∈ V ∧ C ≠ B
16 tpprceq3 ⊢ ¬ C ∈ V ∧ C ≠ B → A B C = A B
17 15 16 syl ⊢ φ ∧ ¬ C ∈ V → A B C = A B
18 2 adantr ⊢ φ ∧ ¬ C ∈ V → A B C ⊆ D
19 17 18 eqsstrrd ⊢ φ ∧ ¬ C ∈ V → A B ⊆ D
20 13 19 prssad ⊢ φ ∧ ¬ C ∈ V → A ∈ D
21 1 adantr ⊢ φ ∧ B ∈ V ∧ C ∈ V → A ∈ V
22 simprl ⊢ φ ∧ B ∈ V ∧ C ∈ V → B ∈ V
23 simprr ⊢ φ ∧ B ∈ V ∧ C ∈ V → C ∈ V
24 2 adantr ⊢ φ ∧ B ∈ V ∧ C ∈ V → A B C ⊆ D
25 tpssg ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D
26 25 biimpar ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A B C ⊆ D → A ∈ D ∧ B ∈ D ∧ C ∈ D
27 21 22 23 24 26 syl31anc ⊢ φ ∧ B ∈ V ∧ C ∈ V → A ∈ D ∧ B ∈ D ∧ C ∈ D
28 27 simp1d ⊢ φ ∧ B ∈ V ∧ C ∈ V → A ∈ D
29 12 20 28 pm2.61dda ⊢ φ → A ∈ D