1stinl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 1stinl		GIF version

Theorem 1stinl 7420

Description: The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)

**Assertion**
Ref	Expression
1stinl	⊢ (𝑋 ∈ 𝑉 → (1^st ‘(inl‘𝑋)) = ∅)

Proof of Theorem 1stinl Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-inl 7393	. . . . 5 ⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
2	1	a1i 9	. . . 4 ⊢ (𝑋 ∈ 𝑉 → inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩))
3		opeq2 3905	. . . . 5 ⊢ (𝑥 = 𝑋 → ⟨∅, 𝑥⟩ = ⟨∅, 𝑋⟩)
4	3	adantl 277	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 = 𝑋) → ⟨∅, 𝑥⟩ = ⟨∅, 𝑋⟩)
5		elex 2833	. . . 4 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V)
6		0ex 4262	. . . . 5 ⊢ ∅ ∈ V
7		opexg 4370	. . . . 5 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝑉) → ⟨∅, 𝑋⟩ ∈ V)
8	6, 7	mpan 428	. . . 4 ⊢ (𝑋 ∈ 𝑉 → ⟨∅, 𝑋⟩ ∈ V)
9	2, 4, 5, 8	fvmptd 5789	. . 3 ⊢ (𝑋 ∈ 𝑉 → (inl‘𝑋) = ⟨∅, 𝑋⟩)
10	9	fveq2d 5702	. 2 ⊢ (𝑋 ∈ 𝑉 → (1^st ‘(inl‘𝑋)) = (1^st ‘⟨∅, 𝑋⟩))
11		op1stg 6388	. . 3 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝑉) → (1^st ‘⟨∅, 𝑋⟩) = ∅)
12	6, 11	mpan 428	. 2 ⊢ (𝑋 ∈ 𝑉 → (1^st ‘⟨∅, 𝑋⟩) = ∅)
13	10, 12	eqtrd 2271	1 ⊢ (𝑋 ∈ 𝑉 → (1^st ‘(inl‘𝑋)) = ∅)

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 = wceq 1402 ∈ wcel 2209 Vcvv 2821 ∅c0 3520 ⟨cop 3712 ↦ cmpt 4193 ‘cfv 5380 1^st c1st 6376 inlcinl 7391

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580

This proof depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-br 4132 df-opab 4194 df-mpt 4195 df-id 4440 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-iota 5340 df-fun 5382 df-fv 5388 df-1st 6378 df-inl 7393

This theorem is used by: djune 7424 updjudhcoinlf 7426 subctctexmid 17235

W3C validator