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 31800
Description: Technical lemma for bnj852 31809. 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 1139 . . . . . . . 8 (𝜒𝜑)
3 bnj594.1 . . . . . . . 8 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
42, 3sylib 219 . . . . . . 7 (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5 bnj594.11 . . . . . . . . 9 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
65simp2bi 1139 . . . . . . . 8 (𝜒′𝜑′)
7 bnj594.9 . . . . . . . 8 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
86, 7sylib 219 . . . . . . 7 (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9 eqtr3 2818 . . . . . . 7 (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
104, 8, 9syl2an 595 . . . . . 6 ((𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11103adant1 1123 . . . . 5 ((𝑛𝐷𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12 fveq2 6538 . . . . . 6 (𝑗 = ∅ → (𝑓𝑗) = (𝑓‘∅))
13 fveq2 6538 . . . . . 6 (𝑗 = ∅ → (𝑔𝑗) = (𝑔‘∅))
1412, 13eqeq12d 2810 . . . . 5 (𝑗 = ∅ → ((𝑓𝑗) = (𝑔𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
1511, 14syl5ibr 247 . . . 4 (𝑗 = ∅ → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
16 bnj594.15 . . . 4 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
1715, 16sylibr 235 . . 3 (𝑗 = ∅ → 𝜃)
1817a1d 25 . 2 (𝑗 = ∅ → ((𝑗𝑛𝜏) → 𝜃))
19 bnj253 31591 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′))
20 bnj252 31590 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ (𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)))
21 anidm 565 . . . . . . 7 ((𝑛𝐷𝑛𝐷) ↔ 𝑛𝐷)
22213anbi1i 1150 . . . . . 6 (((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′) ↔ (𝑛𝐷𝜒𝜒′))
2319, 20, 223bitr3i 302 . . . . 5 ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) ↔ (𝑛𝐷𝜒𝜒′))
24 df-bnj17 31574 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
25 bnj594.17 . . . . . . . . . . . 12 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
2625bnj1095 31670 . . . . . . . . . . 11 (𝜏 → ∀𝑘𝜏)
2726bnj1352 31716 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
2824, 27hbxfrbi 1806 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏))
29 bnj170 31585 . . . . . . . . . . . 12 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅))
30 bnj594.7 . . . . . . . . . . . . . . 15 𝐷 = (ω ∖ {∅})
3130bnj923 31656 . . . . . . . . . . . . . 14 (𝑛𝐷𝑛 ∈ ω)
32 elnn 7446 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛 ∈ ω) → 𝑗 ∈ ω)
3331, 32sylan2 592 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷) → 𝑗 ∈ ω)
3433anim1i 614 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
3529, 34sylbi 218 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36 nnsuc 7453 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37 rexex 3204 . . . . . . . . . . 11 (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → ∃𝑘 𝑗 = suc 𝑘)
3938bnj721 31645 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘 𝑗 = suc 𝑘)
4028, 39bnj596 31634 . . . . . . . 8 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
41 bnj667 31640 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → (𝑗𝑛𝑛𝐷𝜏))
4241anim1i 614 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
43 bnj258 31595 . . . . . . . . . 10 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
4442, 43sylibr 235 . . . . . . . . 9 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏))
45 df-bnj17 31574 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏))
46 bnj219 31620 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘 E 𝑗)
47463ad2ant3 1128 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 E 𝑗)
4847adantr 481 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49 vex 3440 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
5049bnj216 31619 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘𝑗)
51 df-3an 1082 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ ((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷))
52 3anrot 1093 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ (𝑗𝑛𝑛𝐷𝑘𝑗))
53 ancom 461 . . . . . . . . . . . . . . . . . . . 20 (((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
5451, 52, 533bitr3i 302 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑛𝑛𝐷𝑘𝑗) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
55 eldifi 4024 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
5655, 30eleq2s 2901 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝐷𝑛 ∈ ω)
57 nnord 7444 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → Ord 𝑛)
58 ordtr1 6109 . . . . . . . . . . . . . . . . . . . . 21 (Ord 𝑛 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐷 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
6059imp 407 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)) → 𝑘𝑛)
6154, 60sylbi 218 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑛𝑛𝐷𝑘𝑗) → 𝑘𝑛)
6250, 61syl3an3 1158 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘𝑛)
63 rsp 3172 . . . . . . . . . . . . . . . . . 18 (∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃) → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6425, 63sylbi 218 . . . . . . . . . . . . . . . . 17 (𝜏 → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6562, 64mpan9 507 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
6648, 65mpd 15 . . . . . . . . . . . . . . 15 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
6745, 66sylbi 218 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → [𝑘 / 𝑗]𝜃)
6867anim1i 614 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
69 bnj252 31590 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
7068, 69sylibr 235 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′))
71 bnj446 31604 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72 bnj594.16 . . . . . . . . . . . . . 14 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
73 pm3.35 799 . . . . . . . . . . . . . 14 (((𝑛𝐷𝜒𝜒′) ∧ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))) → (𝑓𝑘) = (𝑔𝑘))
7472, 73sylan2b 593 . . . . . . . . . . . . 13 (((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓𝑘) = (𝑔𝑘))
7571, 74sylbi 218 . . . . . . . . . . . 12 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))
76 iuneq1 4840 . . . . . . . . . . . 12 ((𝑓𝑘) = (𝑔𝑘) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
7770, 75, 763syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
78 bnj658 31639 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘))
791simp3bi 1140 . . . . . . . . . . . . . 14 (𝜒𝜓)
805simp3bi 1140 . . . . . . . . . . . . . 14 (𝜒′𝜓′)
8179, 80bnj240 31586 . . . . . . . . . . . . 13 ((𝑛𝐷𝜒𝜒′) → (𝜓𝜓′))
8278, 81anim12i 612 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)))
83 simpl 483 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓)
8483anim2i 616 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓))
85 simp3 1131 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
8685anim1i 614 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘𝜓))
87 simpl1 1184 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → 𝑗𝑛)
88 df-3an 1082 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘))
8988biancomi 463 . . . . . . . . . . . . . . . 16 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
90 elnn 7446 . . . . . . . . . . . . . . . . 17 ((𝑘𝑗𝑗 ∈ ω) → 𝑘 ∈ ω)
9150, 33, 90syl2an 595 . . . . . . . . . . . . . . . 16 ((𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)) → 𝑘 ∈ ω)
9289, 91sylbi 218 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93 bnj594.2 . . . . . . . . . . . . . . . . 17 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
9493bnj589 31797 . . . . . . . . . . . . . . . 16 (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑓‘suc 𝑘) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9594bnj590 31798 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))))
9692, 95mpan9 507 . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓′)
101100anim2i 616 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′))
10285anim1i 614 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘𝜓′))
103 simpl1 1184 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → 𝑗𝑛)
104 bnj594.10 . . . . . . . . . . . . . . . . 17 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
105104bnj589 31797 . . . . . . . . . . . . . . . 16 (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑔‘suc 𝑘) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
106105bnj590 31798 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓′) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))))
10792, 106mpan9 507 . . . . . . . . . . . . . 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 2841 . . . . . . . . . 10 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗))
112111ex 413 . . . . . . . . 9 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11344, 112syl 17 . . . . . . . 8 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11440, 113bnj593 31633 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
115 bnj258 31595 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷))
116 19.9v 1965 . . . . . . 7 (∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)) ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
117114, 115, 1163imtr3i 292 . . . . . 6 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
118117expimpd 454 . . . . 5 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗)))
11923, 118syl5bir 244 . . . 4 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
120119, 16sylibr 235 . . 3 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → 𝜃)
1211203expib 1115 . 2 (𝑗 ≠ ∅ → ((𝑗𝑛𝜏) → 𝜃))
12218, 121pm2.61ine 3068 1 ((𝑗𝑛𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1522  wex 1761  wcel 2081  wne 2984  wral 3105  wrex 3106  [wsbc 3706  cdif 3856  c0 4211  {csn 4472   ciun 4825   class class class wbr 4962   E cep 5352  Ord word 6065  suc csuc 6068   Fn wfn 6220  cfv 6225  ωcom 7436  w-bnj17 31573   predc-bnj14 31575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-tr 5064  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fv 6233  df-om 7437  df-bnj17 31574
This theorem is referenced by:  bnj580  31801
  Copyright terms: Public domain W3C validator