Proof of Theorem bnj594
| Step | Hyp | Ref
| Expression |
| 1 | | bnj594.3 |
. . . . . . . . 9
⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
| 2 | 1 | simp2bi 1147 |
. . . . . . . 8
⊢ (𝜒 → 𝜑) |
| 3 | | bnj594.1 |
. . . . . . . 8
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 4 | 2, 3 | sylib 218 |
. . . . . . 7
⊢ (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 5 | | bnj594.11 |
. . . . . . . . 9
⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) |
| 6 | 5 | simp2bi 1147 |
. . . . . . . 8
⊢ (𝜒′ → 𝜑′) |
| 7 | | bnj594.9 |
. . . . . . . 8
⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 8 | 6, 7 | sylib 218 |
. . . . . . 7
⊢ (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 9 | | eqtr3 2763 |
. . . . . . 7
⊢ (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅)) |
| 10 | 4, 8, 9 | syl2an 596 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅)) |
| 11 | 10 | 3adant1 1131 |
. . . . 5
⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅)) |
| 12 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = ∅ → (𝑓‘𝑗) = (𝑓‘∅)) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = ∅ → (𝑔‘𝑗) = (𝑔‘∅)) |
| 14 | 12, 13 | eqeq12d 2753 |
. . . . 5
⊢ (𝑗 = ∅ → ((𝑓‘𝑗) = (𝑔‘𝑗) ↔ (𝑓‘∅) = (𝑔‘∅))) |
| 15 | 11, 14 | imbitrrid 246 |
. . . 4
⊢ (𝑗 = ∅ → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 16 | | bnj594.15 |
. . . 4
⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 17 | 15, 16 | sylibr 234 |
. . 3
⊢ (𝑗 = ∅ → 𝜃) |
| 18 | 17 | a1d 25 |
. 2
⊢ (𝑗 = ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)) |
| 19 | | bnj253 34718 |
. . . . . 6
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′)) |
| 20 | | bnj252 34717 |
. . . . . 6
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
| 21 | | anidm 564 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ↔ 𝑛 ∈ 𝐷) |
| 22 | 21 | 3anbi1i 1158 |
. . . . . 6
⊢ (((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
| 23 | 19, 20, 22 | 3bitr3i 301 |
. . . . 5
⊢ ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
| 24 | | df-bnj17 34701 |
. . . . . . . . . 10
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏)) |
| 25 | | bnj594.17 |
. . . . . . . . . . . 12
⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) |
| 26 | 25 | bnj1095 34795 |
. . . . . . . . . . 11
⊢ (𝜏 → ∀𝑘𝜏) |
| 27 | 26 | bnj1352 34841 |
. . . . . . . . . 10
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏)) |
| 28 | 24, 27 | hbxfrbi 1825 |
. . . . . . . . 9
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏)) |
| 29 | | bnj170 34712 |
. . . . . . . . . . . 12
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅)) |
| 30 | | bnj594.7 |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = (ω ∖
{∅}) |
| 31 | 30 | bnj923 34782 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
| 32 | | elnn 7898 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω) |
| 33 | 31, 32 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑗 ∈ ω) |
| 34 | 33 | anim1i 615 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅)) |
| 35 | 29, 34 | sylbi 217 |
. . . . . . . . . . 11
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅)) |
| 36 | | nnsuc 7905 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) →
∃𝑘 ∈ ω
𝑗 = suc 𝑘) |
| 37 | | rexex 3076 |
. . . . . . . . . . 11
⊢
(∃𝑘 ∈
ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘) |
| 38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → ∃𝑘 𝑗 = suc 𝑘) |
| 39 | 38 | bnj721 34771 |
. . . . . . . . 9
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘 𝑗 = suc 𝑘) |
| 40 | 28, 39 | bnj596 34760 |
. . . . . . . 8
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
| 41 | | bnj667 34766 |
. . . . . . . . . . 11
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏)) |
| 42 | 41 | anim1i 615 |
. . . . . . . . . 10
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
| 43 | | bnj258 34722 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
| 44 | 42, 43 | sylibr 234 |
. . . . . . . . 9
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏)) |
| 45 | | df-bnj17 34701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏)) |
| 46 | | bnj219 34747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = suc 𝑘 → 𝑘 E 𝑗) |
| 47 | 46 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 E 𝑗) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗) |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑘 ∈ V |
| 50 | 49 | bnj216 34746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗) |
| 51 | | df-3an 1089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷)) |
| 52 | | 3anrot 1100 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗)) |
| 53 | | ancom 460 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛))) |
| 54 | 51, 52, 53 | 3bitr3i 301 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛))) |
| 55 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (ω ∖
{∅}) → 𝑛 ∈
ω) |
| 56 | 55, 30 | eleq2s 2859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
| 57 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ω → Ord 𝑛) |
| 58 | | ordtr1 6427 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Ord
𝑛 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛)) |
| 59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝐷 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛)) |
| 60 | 59 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)) → 𝑘 ∈ 𝑛) |
| 61 | 54, 60 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) → 𝑘 ∈ 𝑛) |
| 62 | 50, 61 | syl3an3 1166 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ 𝑛) |
| 63 | | rsp 3247 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃) → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))) |
| 64 | 25, 63 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜏 → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))) |
| 65 | 62, 64 | mpan9 506 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) |
| 66 | 48, 65 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃) |
| 67 | 45, 66 | sylbi 217 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → [𝑘 / 𝑗]𝜃) |
| 68 | 67 | anim1i 615 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
| 69 | | bnj252 34717 |
. . . . . . . . . . . . 13
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
| 70 | 68, 69 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
| 71 | | bnj446 34731 |
. . . . . . . . . . . . 13
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃)) |
| 72 | | bnj594.16 |
. . . . . . . . . . . . . 14
⊢
([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) |
| 73 | | pm3.35 803 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
| 74 | 72, 73 | sylan2b 594 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
| 75 | 71, 74 | sylbi 217 |
. . . . . . . . . . . 12
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
| 76 | | iuneq1 5008 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑘) = (𝑔‘𝑘) → ∪
𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 77 | 70, 75, 76 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 78 | | bnj658 34765 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘)) |
| 79 | 1 | simp3bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝜓) |
| 80 | 5 | simp3bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝜒′ → 𝜓′) |
| 81 | 79, 80 | bnj240 34713 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝜓 ∧ 𝜓′)) |
| 82 | 78, 81 | anim12i 613 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′))) |
| 83 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜓 ∧ 𝜓′) → 𝜓) |
| 84 | 83 | anim2i 617 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓)) |
| 85 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑗 = suc 𝑘) |
| 86 | 85 | anim1i 615 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘 ∧ 𝜓)) |
| 87 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → 𝑗 ∈ 𝑛) |
| 88 | | df-3an 1089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘)) |
| 89 | 88 | biancomi 462 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))) |
| 90 | | elnn 7898 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω) → 𝑘 ∈ ω) |
| 91 | 50, 33, 90 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) → 𝑘 ∈ ω) |
| 92 | 89, 91 | sylbi 217 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ ω) |
| 93 | | bnj594.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 94 | 93 | bnj589 34923 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
| 95 | 94 | bnj590 34924 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 = suc 𝑘 ∧ 𝜓) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))) |
| 96 | 92, 95 | mpan9 506 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
| 97 | 87, 96 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 98 | 86, 97 | syldan 591 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 99 | 82, 84, 98 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 100 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜓 ∧ 𝜓′) → 𝜓′) |
| 101 | 100 | anim2i 617 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′)) |
| 102 | 85 | anim1i 615 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘 ∧ 𝜓′)) |
| 103 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → 𝑗 ∈ 𝑛) |
| 104 | | bnj594.10 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 105 | 104 | bnj589 34923 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑔‘suc 𝑘) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
| 106 | 105 | bnj590 34924 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 = suc 𝑘 ∧ 𝜓′) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))) |
| 107 | 92, 106 | mpan9 506 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
| 108 | 103, 107 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 109 | 102, 108 | syldan 591 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 110 | 82, 101, 109 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
| 111 | 77, 99, 110 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗)) |
| 112 | 111 | ex 412 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 113 | 44, 112 | syl 17 |
. . . . . . . 8
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 114 | 40, 113 | bnj593 34759 |
. . . . . . 7
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 115 | | bnj258 34722 |
. . . . . . 7
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷)) |
| 116 | | 19.9v 1983 |
. . . . . . 7
⊢
(∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 117 | 114, 115,
116 | 3imtr3i 291 |
. . . . . 6
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 118 | 117 | expimpd 453 |
. . . . 5
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 119 | 23, 118 | biimtrrid 243 |
. . . 4
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
| 120 | 119, 16 | sylibr 234 |
. . 3
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃) |
| 121 | 120 | 3expib 1123 |
. 2
⊢ (𝑗 ≠ ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)) |
| 122 | 18, 121 | pm2.61ine 3025 |
1
⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃) |