ot1stg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ot1stg		Structured version Visualization version GIF version

Theorem ot1stg 8015

Description: Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 8015, ot2ndg 8016, ot3rdg 8017.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)

**Assertion**
Ref	Expression
ot1stg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1^st ‘(1^st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)

**Proof of Theorem ot1stg**
Step	Hyp	Ref	Expression
1		df-ot 4592	. . . . . 6 ⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
2	1	fveq2i 6888	. . . . 5 ⊢ (1^st ‘⟨𝐴, 𝐵, 𝐶⟩) = (1^st ‘⟨⟨𝐴, 𝐵⟩, 𝐶⟩)
3		opex 5431	. . . . . 6 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
4		op1stg 8013	. . . . . 6 ⊢ ((⟨𝐴, 𝐵⟩ ∈ V ∧ 𝐶 ∈ 𝑋) → (1^st ‘⟨⟨𝐴, 𝐵⟩, 𝐶⟩) = ⟨𝐴, 𝐵⟩)
5	3, 4	mpan 703	. . . . 5 ⊢ (𝐶 ∈ 𝑋 → (1^st ‘⟨⟨𝐴, 𝐵⟩, 𝐶⟩) = ⟨𝐴, 𝐵⟩)
6	2, 5	eqtrid 2807	. . . 4 ⊢ (𝐶 ∈ 𝑋 → (1^st ‘⟨𝐴, 𝐵, 𝐶⟩) = ⟨𝐴, 𝐵⟩)
7	6	fveq2d 6889	. . 3 ⊢ (𝐶 ∈ 𝑋 → (1^st ‘(1^st ‘⟨𝐴, 𝐵, 𝐶⟩)) = (1^st ‘⟨𝐴, 𝐵⟩))
8		op1stg 8013	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1^st ‘⟨𝐴, 𝐵⟩) = 𝐴)
9	7, 8	sylan9eqr 2817	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (1^st ‘(1^st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)
10	9	3impa 1127	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1^st ‘(1^st ‘⟨𝐴, 𝐵, 𝐶⟩)) = 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⟨cop 4589 ⟨cotp 4591 ‘cfv 6538 1^st c1st 7999

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-ot 4592 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-iota 6494 df-fun 6540 df-fv 6546 df-1st 8001

This theorem is used by: oteqimp 8020 el2xptp0 8047 sbcoteq1a 8062 xpord3lem 8166 splval 14900 mamufval 22707 msrval 36303 elmsta 36313 mapdhval 42782 hdmap1val 42856

W3C validator