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 33861
Description: Technical lemma for bnj852 33870. 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 1147 . . . . . . . 8 (𝜒𝜑)
3 bnj594.1 . . . . . . . 8 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
42, 3sylib 217 . . . . . . 7 (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5 bnj594.11 . . . . . . . . 9 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
65simp2bi 1147 . . . . . . . 8 (𝜒′𝜑′)
7 bnj594.9 . . . . . . . 8 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
86, 7sylib 217 . . . . . . 7 (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9 eqtr3 2759 . . . . . . 7 (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
104, 8, 9syl2an 597 . . . . . 6 ((𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11103adant1 1131 . . . . 5 ((𝑛𝐷𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12 fveq2 6888 . . . . . 6 (𝑗 = ∅ → (𝑓𝑗) = (𝑓‘∅))
13 fveq2 6888 . . . . . 6 (𝑗 = ∅ → (𝑔𝑗) = (𝑔‘∅))
1412, 13eqeq12d 2749 . . . . 5 (𝑗 = ∅ → ((𝑓𝑗) = (𝑔𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
1511, 14imbitrrid 245 . . . 4 (𝑗 = ∅ → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
16 bnj594.15 . . . 4 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
1715, 16sylibr 233 . . 3 (𝑗 = ∅ → 𝜃)
1817a1d 25 . 2 (𝑗 = ∅ → ((𝑗𝑛𝜏) → 𝜃))
19 bnj253 33653 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′))
20 bnj252 33652 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ (𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)))
21 anidm 566 . . . . . . 7 ((𝑛𝐷𝑛𝐷) ↔ 𝑛𝐷)
22213anbi1i 1158 . . . . . 6 (((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′) ↔ (𝑛𝐷𝜒𝜒′))
2319, 20, 223bitr3i 301 . . . . 5 ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) ↔ (𝑛𝐷𝜒𝜒′))
24 df-bnj17 33636 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
25 bnj594.17 . . . . . . . . . . . 12 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
2625bnj1095 33730 . . . . . . . . . . 11 (𝜏 → ∀𝑘𝜏)
2726bnj1352 33776 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
2824, 27hbxfrbi 1828 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏))
29 bnj170 33647 . . . . . . . . . . . 12 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅))
30 bnj594.7 . . . . . . . . . . . . . . 15 𝐷 = (ω ∖ {∅})
3130bnj923 33717 . . . . . . . . . . . . . 14 (𝑛𝐷𝑛 ∈ ω)
32 elnn 7861 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛 ∈ ω) → 𝑗 ∈ ω)
3331, 32sylan2 594 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷) → 𝑗 ∈ ω)
3433anim1i 616 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
3529, 34sylbi 216 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36 nnsuc 7868 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37 rexex 3077 . . . . . . . . . . 11 (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → ∃𝑘 𝑗 = suc 𝑘)
3938bnj721 33706 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘 𝑗 = suc 𝑘)
4028, 39bnj596 33695 . . . . . . . 8 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
41 bnj667 33701 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → (𝑗𝑛𝑛𝐷𝜏))
4241anim1i 616 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
43 bnj258 33657 . . . . . . . . . 10 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
4442, 43sylibr 233 . . . . . . . . 9 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏))
45 df-bnj17 33636 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏))
46 bnj219 33682 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘 E 𝑗)
47463ad2ant3 1136 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 E 𝑗)
4847adantr 482 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49 vex 3479 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
5049bnj216 33681 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘𝑗)
51 df-3an 1090 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ ((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷))
52 3anrot 1101 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ (𝑗𝑛𝑛𝐷𝑘𝑗))
53 ancom 462 . . . . . . . . . . . . . . . . . . . 20 (((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
5451, 52, 533bitr3i 301 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑛𝑛𝐷𝑘𝑗) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
55 eldifi 4125 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
5655, 30eleq2s 2852 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝐷𝑛 ∈ ω)
57 nnord 7858 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → Ord 𝑛)
58 ordtr1 6404 . . . . . . . . . . . . . . . . . . . . 21 (Ord 𝑛 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐷 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
6059imp 408 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)) → 𝑘𝑛)
6154, 60sylbi 216 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑛𝑛𝐷𝑘𝑗) → 𝑘𝑛)
6250, 61syl3an3 1166 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘𝑛)
63 rsp 3245 . . . . . . . . . . . . . . . . . 18 (∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃) → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6425, 63sylbi 216 . . . . . . . . . . . . . . . . 17 (𝜏 → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6562, 64mpan9 508 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
6648, 65mpd 15 . . . . . . . . . . . . . . 15 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
6745, 66sylbi 216 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → [𝑘 / 𝑗]𝜃)
6867anim1i 616 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
69 bnj252 33652 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
7068, 69sylibr 233 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′))
71 bnj446 33666 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72 bnj594.16 . . . . . . . . . . . . . 14 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
73 pm3.35 802 . . . . . . . . . . . . . 14 (((𝑛𝐷𝜒𝜒′) ∧ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))) → (𝑓𝑘) = (𝑔𝑘))
7472, 73sylan2b 595 . . . . . . . . . . . . 13 (((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓𝑘) = (𝑔𝑘))
7571, 74sylbi 216 . . . . . . . . . . . 12 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))
76 iuneq1 5012 . . . . . . . . . . . 12 ((𝑓𝑘) = (𝑔𝑘) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
7770, 75, 763syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
78 bnj658 33700 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘))
791simp3bi 1148 . . . . . . . . . . . . . 14 (𝜒𝜓)
805simp3bi 1148 . . . . . . . . . . . . . 14 (𝜒′𝜓′)
8179, 80bnj240 33648 . . . . . . . . . . . . 13 ((𝑛𝐷𝜒𝜒′) → (𝜓𝜓′))
8278, 81anim12i 614 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)))
83 simpl 484 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓)
8483anim2i 618 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓))
85 simp3 1139 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
8685anim1i 616 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘𝜓))
87 simpl1 1192 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → 𝑗𝑛)
88 df-3an 1090 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘))
8988biancomi 464 . . . . . . . . . . . . . . . 16 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
90 elnn 7861 . . . . . . . . . . . . . . . . 17 ((𝑘𝑗𝑗 ∈ ω) → 𝑘 ∈ ω)
9150, 33, 90syl2an 597 . . . . . . . . . . . . . . . 16 ((𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)) → 𝑘 ∈ ω)
9289, 91sylbi 216 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93 bnj594.2 . . . . . . . . . . . . . . . . 17 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
9493bnj589 33858 . . . . . . . . . . . . . . . 16 (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑓‘suc 𝑘) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9594bnj590 33859 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))))
9692, 95mpan9 508 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9787, 96mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9886, 97syldan 592 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9982, 84, 983syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
100 simpr 486 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓′)
101100anim2i 618 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′))
10285anim1i 616 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘𝜓′))
103 simpl1 1192 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → 𝑗𝑛)
104 bnj594.10 . . . . . . . . . . . . . . . . 17 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
105104bnj589 33858 . . . . . . . . . . . . . . . 16 (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑔‘suc 𝑘) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
106105bnj590 33859 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓′) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))))
10792, 106mpan9 508 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
108103, 107mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
109102, 108syldan 592 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11082, 101, 1093syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11177, 99, 1103eqtr4d 2783 . . . . . . . . . 10 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗))
112111ex 414 . . . . . . . . 9 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11344, 112syl 17 . . . . . . . 8 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11440, 113bnj593 33694 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
115 bnj258 33657 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷))
116 19.9v 1988 . . . . . . 7 (∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)) ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
117114, 115, 1163imtr3i 291 . . . . . 6 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
118117expimpd 455 . . . . 5 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗)))
11923, 118biimtrrid 242 . . . 4 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
120119, 16sylibr 233 . . 3 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → 𝜃)
1211203expib 1123 . 2 (𝑗 ≠ ∅ → ((𝑗𝑛𝜏) → 𝜃))
12218, 121pm2.61ine 3026 1 ((𝑗𝑛𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wne 2941  wral 3062  wrex 3071  [wsbc 3776  cdif 3944  c0 4321  {csn 4627   ciun 4996   class class class wbr 5147   E cep 5578  Ord word 6360  suc csuc 6363   Fn wfn 6535  cfv 6540  ωcom 7850  w-bnj17 33635   predc-bnj14 33637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fv 6548  df-om 7851  df-bnj17 33636
This theorem is referenced by:  bnj580  33862
  Copyright terms: Public domain W3C validator