Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eliniseg | Structured version Visualization version GIF version |
Description: Membership in an initial segment. The idiom (◡𝐴 “ {𝐵}), meaning {𝑥 ∣ 𝑥𝐴𝐵}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
eliniseg.1 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
eliniseg | ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliniseg.1 | . 2 ⊢ 𝐶 ∈ V | |
2 | elimasng 5930 | . . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 〈𝐵, 𝐶〉 ∈ ◡𝐴)) | |
3 | df-br 5032 | . . . 4 ⊢ (𝐵◡𝐴𝐶 ↔ 〈𝐵, 𝐶〉 ∈ ◡𝐴) | |
4 | 2, 3 | bitr4di 292 | . . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐵◡𝐴𝐶)) |
5 | brcnvg 5723 | . . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐵◡𝐴𝐶 ↔ 𝐶𝐴𝐵)) | |
6 | 4, 5 | bitrd 282 | . 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) |
7 | 1, 6 | mpan2 691 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2113 Vcvv 3398 {csn 4517 〈cop 4523 class class class wbr 5031 ◡ccnv 5525 “ cima 5529 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 df-xp 5532 df-cnv 5534 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 |
This theorem is referenced by: epini 5934 iniseg 5935 dfco2a 6080 elpred 6143 isomin 7104 isoini 7105 fnse 7854 infxpenlem 9514 fpwwe2lem7 10138 fpwwe2lem11 10142 fpwwe2lem12 10143 fpwwe2 10144 canth4 10148 canthwelem 10151 pwfseqlem4 10163 fz1isolem 13914 itg1addlem4 24452 elnlfn 29863 pw2f1ocnv 40423 |
Copyright terms: Public domain | W3C validator |