![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj518 | Structured version Visualization version GIF version |
Description: Technical lemma for bnj852 31846. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bnj518.1 | ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
bnj518.2 | ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
bnj518.3 | ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛)) |
Ref | Expression |
---|---|
bnj518 | ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj518.3 | . . . 4 ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛)) | |
2 | bnj334 31637 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛) ↔ (𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛)) | |
3 | 1, 2 | bitri 267 | . . 3 ⊢ (𝜏 ↔ (𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛)) |
4 | df-bnj17 31611 | . . . 4 ⊢ ((𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛) ↔ ((𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑝 ∈ 𝑛)) | |
5 | bnj518.1 | . . . . . 6 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) | |
6 | bnj518.2 | . . . . . 6 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | |
7 | 5, 6 | bnj517 31810 | . . . . 5 ⊢ ((𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑝 ∈ 𝑛 (𝑓‘𝑝) ⊆ 𝐴) |
8 | 7 | r19.21bi 3158 | . . . 4 ⊢ (((𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑝 ∈ 𝑛) → (𝑓‘𝑝) ⊆ 𝐴) |
9 | 4, 8 | sylbi 209 | . . 3 ⊢ ((𝑛 ∈ ω ∧ 𝜑 ∧ 𝜓 ∧ 𝑝 ∈ 𝑛) → (𝑓‘𝑝) ⊆ 𝐴) |
10 | 3, 9 | sylbi 209 | . 2 ⊢ (𝜏 → (𝑓‘𝑝) ⊆ 𝐴) |
11 | ssel 3852 | . . . 4 ⊢ ((𝑓‘𝑝) ⊆ 𝐴 → (𝑦 ∈ (𝑓‘𝑝) → 𝑦 ∈ 𝐴)) | |
12 | bnj93 31788 | . . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴) → pred(𝑦, 𝐴, 𝑅) ∈ V) | |
13 | 12 | ex 405 | . . . 4 ⊢ (𝑅 FrSe 𝐴 → (𝑦 ∈ 𝐴 → pred(𝑦, 𝐴, 𝑅) ∈ V)) |
14 | 11, 13 | sylan9r 501 | . . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ (𝑓‘𝑝) ⊆ 𝐴) → (𝑦 ∈ (𝑓‘𝑝) → pred(𝑦, 𝐴, 𝑅) ∈ V)) |
15 | 14 | ralrimiv 3131 | . 2 ⊢ ((𝑅 FrSe 𝐴 ∧ (𝑓‘𝑝) ⊆ 𝐴) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) |
16 | 10, 15 | sylan2 583 | 1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∀wral 3088 Vcvv 3415 ⊆ wss 3829 ∅c0 4178 ∪ ciun 4792 suc csuc 6031 ‘cfv 6188 ωcom 7396 ∧ w-bnj17 31610 predc-bnj14 31612 FrSe w-bnj15 31616 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 ax-un 7279 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-tr 5031 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fv 6196 df-om 7397 df-bnj17 31611 df-bnj14 31613 df-bnj13 31615 df-bnj15 31617 |
This theorem is referenced by: bnj535 31815 bnj546 31821 |
Copyright terms: Public domain | W3C validator |