![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj1529 | Structured version Visualization version GIF version |
Description: Technical lemma for bnj1522 34549. 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 |
---|---|
bnj1529.1 | ⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
bnj1529.2 | ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) |
Ref | Expression |
---|---|
bnj1529 | ⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1529.1 | . 2 ⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) | |
2 | nfv 1916 | . . 3 ⊢ Ⅎ𝑦(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) | |
3 | bnj1529.2 | . . . . . 6 ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) | |
4 | 3 | nfcii 2886 | . . . . 5 ⊢ Ⅎ𝑥𝐹 |
5 | nfcv 2902 | . . . . 5 ⊢ Ⅎ𝑥𝑦 | |
6 | 4, 5 | nffv 6901 | . . . 4 ⊢ Ⅎ𝑥(𝐹‘𝑦) |
7 | nfcv 2902 | . . . . 5 ⊢ Ⅎ𝑥𝐺 | |
8 | nfcv 2902 | . . . . . . 7 ⊢ Ⅎ𝑥 pred(𝑦, 𝐴, 𝑅) | |
9 | 4, 8 | nfres 5983 | . . . . . 6 ⊢ Ⅎ𝑥(𝐹 ↾ pred(𝑦, 𝐴, 𝑅)) |
10 | 5, 9 | nfop 4889 | . . . . 5 ⊢ Ⅎ𝑥⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩ |
11 | 7, 10 | nffv 6901 | . . . 4 ⊢ Ⅎ𝑥(𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩) |
12 | 6, 11 | nfeq 2915 | . . 3 ⊢ Ⅎ𝑥(𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩) |
13 | fveq2 6891 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) | |
14 | id 22 | . . . . . 6 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | |
15 | bnj602 34392 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → pred(𝑥, 𝐴, 𝑅) = pred(𝑦, 𝐴, 𝑅)) | |
16 | 15 | reseq2d 5981 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))) |
17 | 14, 16 | opeq12d 4881 | . . . . 5 ⊢ (𝑥 = 𝑦 → ⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩ = ⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩) |
18 | 17 | fveq2d 6895 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩)) |
19 | 13, 18 | eqeq12d 2747 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) ↔ (𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩))) |
20 | 2, 12, 19 | cbvralw 3302 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) ↔ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩)) |
21 | 1, 20 | sylib 217 | 1 ⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘⟨𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))⟩)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1538 = wceq 1540 ∈ wcel 2105 ∀wral 3060 ⟨cop 4634 ↾ cres 5678 ‘cfv 6543 predc-bnj14 34165 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-xp 5682 df-res 5688 df-iota 6495 df-fv 6551 df-bnj14 34166 |
This theorem is referenced by: bnj1523 34548 |
Copyright terms: Public domain | W3C validator |