Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj594 Structured version   Visualization version   GIF version

Theorem bnj594 34904
Description: Technical lemma for bnj852 34913. 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.)
Hypotheses
Ref Expression
bnj594.1 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.2 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.3 (𝜒 ↔ (𝑓 Fn 𝑛𝜑𝜓))
bnj594.7 𝐷 = (ω ∖ {∅})
bnj594.9 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.10 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.11 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
bnj594.15 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
bnj594.16 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
bnj594.17 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
Assertion
Ref Expression
bnj594 ((𝑗𝑛𝜏) → 𝜃)
Distinct variable groups:   𝐴,𝑖,𝑘   𝐷,𝑘   𝑅,𝑖,𝑘   𝜒,𝑘   𝑘,𝜒′   𝑓,𝑖,𝑘,𝑦   𝑔,𝑖,𝑘,𝑦   𝑖,𝑛,𝑘   𝑗,𝑘
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)   𝜃(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜏(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝐴(𝑥,𝑦,𝑓,𝑔,𝑗,𝑛)   𝐷(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)   𝑅(𝑥,𝑦,𝑓,𝑔,𝑗,𝑛)   𝜑′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜓′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜒′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)

Proof of Theorem bnj594
StepHypRef Expression
1 bnj594.3 . . . . . . . . 9 (𝜒 ↔ (𝑓 Fn 𝑛𝜑𝜓))
21simp2bi 1145 . . . . . . . 8 (𝜒𝜑)
3 bnj594.1 . . . . . . . 8 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
42, 3sylib 218 . . . . . . 7 (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5 bnj594.11 . . . . . . . . 9 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
65simp2bi 1145 . . . . . . . 8 (𝜒′𝜑′)
7 bnj594.9 . . . . . . . 8 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
86, 7sylib 218 . . . . . . 7 (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9 eqtr3 2760 . . . . . . 7 (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
104, 8, 9syl2an 596 . . . . . 6 ((𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11103adant1 1129 . . . . 5 ((𝑛𝐷𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12 fveq2 6906 . . . . . 6 (𝑗 = ∅ → (𝑓𝑗) = (𝑓‘∅))
13 fveq2 6906 . . . . . 6 (𝑗 = ∅ → (𝑔𝑗) = (𝑔‘∅))
1412, 13eqeq12d 2750 . . . . 5 (𝑗 = ∅ → ((𝑓𝑗) = (𝑔𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
1511, 14imbitrrid 246 . . . 4 (𝑗 = ∅ → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
16 bnj594.15 . . . 4 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
1715, 16sylibr 234 . . 3 (𝑗 = ∅ → 𝜃)
1817a1d 25 . 2 (𝑗 = ∅ → ((𝑗𝑛𝜏) → 𝜃))
19 bnj253 34696 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′))
20 bnj252 34695 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ (𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)))
21 anidm 564 . . . . . . 7 ((𝑛𝐷𝑛𝐷) ↔ 𝑛𝐷)
22213anbi1i 1156 . . . . . 6 (((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′) ↔ (𝑛𝐷𝜒𝜒′))
2319, 20, 223bitr3i 301 . . . . 5 ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) ↔ (𝑛𝐷𝜒𝜒′))
24 df-bnj17 34679 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
25 bnj594.17 . . . . . . . . . . . 12 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
2625bnj1095 34773 . . . . . . . . . . 11 (𝜏 → ∀𝑘𝜏)
2726bnj1352 34819 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
2824, 27hbxfrbi 1821 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏))
29 bnj170 34690 . . . . . . . . . . . 12 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅))
30 bnj594.7 . . . . . . . . . . . . . . 15 𝐷 = (ω ∖ {∅})
3130bnj923 34760 . . . . . . . . . . . . . 14 (𝑛𝐷𝑛 ∈ ω)
32 elnn 7897 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛 ∈ ω) → 𝑗 ∈ ω)
3331, 32sylan2 593 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷) → 𝑗 ∈ ω)
3433anim1i 615 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
3529, 34sylbi 217 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36 nnsuc 7904 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37 rexex 3073 . . . . . . . . . . 11 (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → ∃𝑘 𝑗 = suc 𝑘)
3938bnj721 34749 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘 𝑗 = suc 𝑘)
4028, 39bnj596 34738 . . . . . . . 8 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
41 bnj667 34744 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → (𝑗𝑛𝑛𝐷𝜏))
4241anim1i 615 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
43 bnj258 34700 . . . . . . . . . 10 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
4442, 43sylibr 234 . . . . . . . . 9 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏))
45 df-bnj17 34679 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏))
46 bnj219 34725 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘 E 𝑗)
47463ad2ant3 1134 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 E 𝑗)
4847adantr 480 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49 vex 3481 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
5049bnj216 34724 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘𝑗)
51 df-3an 1088 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ ((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷))
52 3anrot 1099 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ (𝑗𝑛𝑛𝐷𝑘𝑗))
53 ancom 460 . . . . . . . . . . . . . . . . . . . 20 (((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
5451, 52, 533bitr3i 301 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑛𝑛𝐷𝑘𝑗) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
55 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
5655, 30eleq2s 2856 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝐷𝑛 ∈ ω)
57 nnord 7894 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → Ord 𝑛)
58 ordtr1 6428 . . . . . . . . . . . . . . . . . . . . 21 (Ord 𝑛 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐷 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
6059imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)) → 𝑘𝑛)
6154, 60sylbi 217 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑛𝑛𝐷𝑘𝑗) → 𝑘𝑛)
6250, 61syl3an3 1164 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘𝑛)
63 rsp 3244 . . . . . . . . . . . . . . . . . 18 (∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃) → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6425, 63sylbi 217 . . . . . . . . . . . . . . . . 17 (𝜏 → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6562, 64mpan9 506 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
6648, 65mpd 15 . . . . . . . . . . . . . . 15 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
6745, 66sylbi 217 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → [𝑘 / 𝑗]𝜃)
6867anim1i 615 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
69 bnj252 34695 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
7068, 69sylibr 234 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′))
71 bnj446 34709 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72 bnj594.16 . . . . . . . . . . . . . 14 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
73 pm3.35 803 . . . . . . . . . . . . . 14 (((𝑛𝐷𝜒𝜒′) ∧ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))) → (𝑓𝑘) = (𝑔𝑘))
7472, 73sylan2b 594 . . . . . . . . . . . . 13 (((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓𝑘) = (𝑔𝑘))
7571, 74sylbi 217 . . . . . . . . . . . 12 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))
76 iuneq1 5012 . . . . . . . . . . . 12 ((𝑓𝑘) = (𝑔𝑘) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
7770, 75, 763syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
78 bnj658 34743 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘))
791simp3bi 1146 . . . . . . . . . . . . . 14 (𝜒𝜓)
805simp3bi 1146 . . . . . . . . . . . . . 14 (𝜒′𝜓′)
8179, 80bnj240 34691 . . . . . . . . . . . . 13 ((𝑛𝐷𝜒𝜒′) → (𝜓𝜓′))
8278, 81anim12i 613 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)))
83 simpl 482 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓)
8483anim2i 617 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓))
85 simp3 1137 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
8685anim1i 615 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘𝜓))
87 simpl1 1190 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → 𝑗𝑛)
88 df-3an 1088 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘))
8988biancomi 462 . . . . . . . . . . . . . . . 16 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
90 elnn 7897 . . . . . . . . . . . . . . . . 17 ((𝑘𝑗𝑗 ∈ ω) → 𝑘 ∈ ω)
9150, 33, 90syl2an 596 . . . . . . . . . . . . . . . 16 ((𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)) → 𝑘 ∈ ω)
9289, 91sylbi 217 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93 bnj594.2 . . . . . . . . . . . . . . . . 17 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
9493bnj589 34901 . . . . . . . . . . . . . . . 16 (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑓‘suc 𝑘) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9594bnj590 34902 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))))
9692, 95mpan9 506 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9787, 96mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9886, 97syldan 591 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9982, 84, 983syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
100 simpr 484 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓′)
101100anim2i 617 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′))
10285anim1i 615 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘𝜓′))
103 simpl1 1190 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → 𝑗𝑛)
104 bnj594.10 . . . . . . . . . . . . . . . . 17 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
105104bnj589 34901 . . . . . . . . . . . . . . . 16 (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑔‘suc 𝑘) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
106105bnj590 34902 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓′) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))))
10792, 106mpan9 506 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
108103, 107mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
109102, 108syldan 591 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11082, 101, 1093syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11177, 99, 1103eqtr4d 2784 . . . . . . . . . 10 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗))
112111ex 412 . . . . . . . . 9 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11344, 112syl 17 . . . . . . . 8 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11440, 113bnj593 34737 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
115 bnj258 34700 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷))
116 19.9v 1980 . . . . . . 7 (∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)) ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
117114, 115, 1163imtr3i 291 . . . . . 6 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
118117expimpd 453 . . . . 5 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗)))
11923, 118biimtrrid 243 . . . 4 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
120119, 16sylibr 234 . . 3 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → 𝜃)
1211203expib 1121 . 2 (𝑗 ≠ ∅ → ((𝑗𝑛𝜏) → 𝜃))
12218, 121pm2.61ine 3022 1 ((𝑗𝑛𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  wrex 3067  [wsbc 3790  cdif 3959  c0 4338  {csn 4630   ciun 4995   class class class wbr 5147   E cep 5587  Ord word 6384  suc csuc 6387   Fn wfn 6557  cfv 6562  ωcom 7886  w-bnj17 34678   predc-bnj14 34680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fv 6570  df-om 7887  df-bnj17 34679
This theorem is referenced by:  bnj580  34905
  Copyright terms: Public domain W3C validator