Proof of Theorem bnj594
Step | Hyp | Ref
| Expression |
1 | | bnj594.3 |
. . . . . . . . 9
⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
2 | 1 | simp2bi 1148 |
. . . . . . . 8
⊢ (𝜒 → 𝜑) |
3 | | bnj594.1 |
. . . . . . . 8
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
4 | 2, 3 | sylib 221 |
. . . . . . 7
⊢ (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
5 | | bnj594.11 |
. . . . . . . . 9
⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)) |
6 | 5 | simp2bi 1148 |
. . . . . . . 8
⊢ (𝜒′ → 𝜑′) |
7 | | bnj594.9 |
. . . . . . . 8
⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) |
8 | 6, 7 | sylib 221 |
. . . . . . 7
⊢ (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) |
9 | | eqtr3 2763 |
. . . . . . 7
⊢ (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅)) |
10 | 4, 8, 9 | syl2an 599 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅)) |
11 | 10 | 3adant1 1132 |
. . . . 5
⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅)) |
12 | | fveq2 6717 |
. . . . . 6
⊢ (𝑗 = ∅ → (𝑓‘𝑗) = (𝑓‘∅)) |
13 | | fveq2 6717 |
. . . . . 6
⊢ (𝑗 = ∅ → (𝑔‘𝑗) = (𝑔‘∅)) |
14 | 12, 13 | eqeq12d 2753 |
. . . . 5
⊢ (𝑗 = ∅ → ((𝑓‘𝑗) = (𝑔‘𝑗) ↔ (𝑓‘∅) = (𝑔‘∅))) |
15 | 11, 14 | syl5ibr 249 |
. . . 4
⊢ (𝑗 = ∅ → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
16 | | bnj594.15 |
. . . 4
⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
17 | 15, 16 | sylibr 237 |
. . 3
⊢ (𝑗 = ∅ → 𝜃) |
18 | 17 | a1d 25 |
. 2
⊢ (𝑗 = ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)) |
19 | | bnj253 32395 |
. . . . . 6
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′)) |
20 | | bnj252 32394 |
. . . . . 6
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
21 | | anidm 568 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ↔ 𝑛 ∈ 𝐷) |
22 | 21 | 3anbi1i 1159 |
. . . . . 6
⊢ (((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
23 | 19, 20, 22 | 3bitr3i 304 |
. . . . 5
⊢ ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
24 | | df-bnj17 32378 |
. . . . . . . . . 10
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏)) |
25 | | bnj594.17 |
. . . . . . . . . . . 12
⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) |
26 | 25 | bnj1095 32474 |
. . . . . . . . . . 11
⊢ (𝜏 → ∀𝑘𝜏) |
27 | 26 | bnj1352 32520 |
. . . . . . . . . 10
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏)) |
28 | 24, 27 | hbxfrbi 1832 |
. . . . . . . . 9
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏)) |
29 | | bnj170 32389 |
. . . . . . . . . . . 12
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅)) |
30 | | bnj594.7 |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = (ω ∖
{∅}) |
31 | 30 | bnj923 32460 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
32 | | elnn 7655 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω) |
33 | 31, 32 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑗 ∈ ω) |
34 | 33 | anim1i 618 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅)) |
35 | 29, 34 | sylbi 220 |
. . . . . . . . . . 11
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅)) |
36 | | nnsuc 7662 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) →
∃𝑘 ∈ ω
𝑗 = suc 𝑘) |
37 | | rexex 3162 |
. . . . . . . . . . 11
⊢
(∃𝑘 ∈
ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → ∃𝑘 𝑗 = suc 𝑘) |
39 | 38 | bnj721 32449 |
. . . . . . . . 9
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘 𝑗 = suc 𝑘) |
40 | 28, 39 | bnj596 32438 |
. . . . . . . 8
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
41 | | bnj667 32444 |
. . . . . . . . . . 11
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏)) |
42 | 41 | anim1i 618 |
. . . . . . . . . 10
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
43 | | bnj258 32399 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘)) |
44 | 42, 43 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏)) |
45 | | df-bnj17 32378 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏)) |
46 | | bnj219 32424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = suc 𝑘 → 𝑘 E 𝑗) |
47 | 46 | 3ad2ant3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 E 𝑗) |
48 | 47 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗) |
49 | | vex 3412 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑘 ∈ V |
50 | 49 | bnj216 32423 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗) |
51 | | df-3an 1091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷)) |
52 | | 3anrot 1102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗)) |
53 | | ancom 464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛))) |
54 | 51, 52, 53 | 3bitr3i 304 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛))) |
55 | | eldifi 4041 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (ω ∖
{∅}) → 𝑛 ∈
ω) |
56 | 55, 30 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω) |
57 | | nnord 7652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ω → Ord 𝑛) |
58 | | ordtr1 6256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Ord
𝑛 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛)) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝐷 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛)) |
60 | 59 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)) → 𝑘 ∈ 𝑛) |
61 | 54, 60 | sylbi 220 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) → 𝑘 ∈ 𝑛) |
62 | 50, 61 | syl3an3 1167 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ 𝑛) |
63 | | rsp 3127 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃) → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))) |
64 | 25, 63 | sylbi 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜏 → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))) |
65 | 62, 64 | mpan9 510 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)) |
66 | 48, 65 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃) |
67 | 45, 66 | sylbi 220 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → [𝑘 / 𝑗]𝜃) |
68 | 67 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
69 | | bnj252 32394 |
. . . . . . . . . . . . 13
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))) |
70 | 68, 69 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) |
71 | | bnj446 32408 |
. . . . . . . . . . . . 13
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃)) |
72 | | bnj594.16 |
. . . . . . . . . . . . . 14
⊢
([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) |
73 | | pm3.35 803 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
74 | 72, 73 | sylan2b 597 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
75 | 71, 74 | sylbi 220 |
. . . . . . . . . . . 12
⊢
(([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)) |
76 | | iuneq1 4920 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑘) = (𝑔‘𝑘) → ∪
𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
77 | 70, 75, 76 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
78 | | bnj658 32443 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘)) |
79 | 1 | simp3bi 1149 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝜓) |
80 | 5 | simp3bi 1149 |
. . . . . . . . . . . . . 14
⊢ (𝜒′ → 𝜓′) |
81 | 79, 80 | bnj240 32390 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝜓 ∧ 𝜓′)) |
82 | 78, 81 | anim12i 616 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′))) |
83 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝜓 ∧ 𝜓′) → 𝜓) |
84 | 83 | anim2i 620 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓)) |
85 | | simp3 1140 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑗 = suc 𝑘) |
86 | 85 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘 ∧ 𝜓)) |
87 | | simpl1 1193 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → 𝑗 ∈ 𝑛) |
88 | | df-3an 1091 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘)) |
89 | 88 | biancomi 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))) |
90 | | elnn 7655 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω) → 𝑘 ∈ ω) |
91 | 50, 33, 90 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) → 𝑘 ∈ ω) |
92 | 89, 91 | sylbi 220 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ ω) |
93 | | bnj594.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
94 | 93 | bnj589 32602 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
95 | 94 | bnj590 32603 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 = suc 𝑘 ∧ 𝜓) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))) |
96 | 92, 95 | mpan9 510 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
97 | 87, 96 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
98 | 86, 97 | syldan 594 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
99 | 82, 84, 98 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
100 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜓 ∧ 𝜓′) → 𝜓′) |
101 | 100 | anim2i 620 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′)) |
102 | 85 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘 ∧ 𝜓′)) |
103 | | simpl1 1193 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → 𝑗 ∈ 𝑛) |
104 | | bnj594.10 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
105 | 104 | bnj589 32602 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑔‘suc 𝑘) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
106 | 105 | bnj590 32603 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 = suc 𝑘 ∧ 𝜓′) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))) |
107 | 92, 106 | mpan9 510 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))) |
108 | 103, 107 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
109 | 102, 108 | syldan 594 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
110 | 82, 101, 109 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)) |
111 | 77, 99, 110 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗)) |
112 | 111 | ex 416 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
113 | 44, 112 | syl 17 |
. . . . . . . 8
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
114 | 40, 113 | bnj593 32437 |
. . . . . . 7
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
115 | | bnj258 32399 |
. . . . . . 7
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷)) |
116 | | 19.9v 1992 |
. . . . . . 7
⊢
(∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
117 | 114, 115,
116 | 3imtr3i 294 |
. . . . . 6
⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
118 | 117 | expimpd 457 |
. . . . 5
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
119 | 23, 118 | syl5bir 246 |
. . . 4
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗))) |
120 | 119, 16 | sylibr 237 |
. . 3
⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃) |
121 | 120 | 3expib 1124 |
. 2
⊢ (𝑗 ≠ ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)) |
122 | 18, 121 | pm2.61ine 3025 |
1
⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃) |