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 32360
 Description: Technical lemma for bnj852 32369. 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 1143 . . . . . . . 8 (𝜒𝜑)
3 bnj594.1 . . . . . . . 8 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
42, 3sylib 221 . . . . . . 7 (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5 bnj594.11 . . . . . . . . 9 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
65simp2bi 1143 . . . . . . . 8 (𝜒′𝜑′)
7 bnj594.9 . . . . . . . 8 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
86, 7sylib 221 . . . . . . 7 (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9 eqtr3 2820 . . . . . . 7 (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
104, 8, 9syl2an 598 . . . . . 6 ((𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11103adant1 1127 . . . . 5 ((𝑛𝐷𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12 fveq2 6655 . . . . . 6 (𝑗 = ∅ → (𝑓𝑗) = (𝑓‘∅))
13 fveq2 6655 . . . . . 6 (𝑗 = ∅ → (𝑔𝑗) = (𝑔‘∅))
1412, 13eqeq12d 2814 . . . . 5 (𝑗 = ∅ → ((𝑓𝑗) = (𝑔𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
1511, 14syl5ibr 249 . . . 4 (𝑗 = ∅ → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
16 bnj594.15 . . . 4 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
1715, 16sylibr 237 . . 3 (𝑗 = ∅ → 𝜃)
1817a1d 25 . 2 (𝑗 = ∅ → ((𝑗𝑛𝜏) → 𝜃))
19 bnj253 32150 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′))
20 bnj252 32149 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ (𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)))
21 anidm 568 . . . . . . 7 ((𝑛𝐷𝑛𝐷) ↔ 𝑛𝐷)
22213anbi1i 1154 . . . . . 6 (((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′) ↔ (𝑛𝐷𝜒𝜒′))
2319, 20, 223bitr3i 304 . . . . 5 ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) ↔ (𝑛𝐷𝜒𝜒′))
24 df-bnj17 32133 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
25 bnj594.17 . . . . . . . . . . . 12 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
2625bnj1095 32229 . . . . . . . . . . 11 (𝜏 → ∀𝑘𝜏)
2726bnj1352 32275 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
2824, 27hbxfrbi 1826 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏))
29 bnj170 32144 . . . . . . . . . . . 12 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅))
30 bnj594.7 . . . . . . . . . . . . . . 15 𝐷 = (ω ∖ {∅})
3130bnj923 32215 . . . . . . . . . . . . . 14 (𝑛𝐷𝑛 ∈ ω)
32 elnn 7583 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛 ∈ ω) → 𝑗 ∈ ω)
3331, 32sylan2 595 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷) → 𝑗 ∈ ω)
3433anim1i 617 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
3529, 34sylbi 220 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36 nnsuc 7590 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37 rexex 3203 . . . . . . . . . . 11 (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → ∃𝑘 𝑗 = suc 𝑘)
3938bnj721 32204 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘 𝑗 = suc 𝑘)
4028, 39bnj596 32193 . . . . . . . 8 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
41 bnj667 32199 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → (𝑗𝑛𝑛𝐷𝜏))
4241anim1i 617 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
43 bnj258 32154 . . . . . . . . . 10 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
4442, 43sylibr 237 . . . . . . . . 9 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏))
45 df-bnj17 32133 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏))
46 bnj219 32179 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘 E 𝑗)
47463ad2ant3 1132 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 E 𝑗)
4847adantr 484 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49 vex 3445 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
5049bnj216 32178 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘𝑗)
51 df-3an 1086 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ ((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷))
52 3anrot 1097 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ (𝑗𝑛𝑛𝐷𝑘𝑗))
53 ancom 464 . . . . . . . . . . . . . . . . . . . 20 (((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
5451, 52, 533bitr3i 304 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑛𝑛𝐷𝑘𝑗) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
55 eldifi 4057 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
5655, 30eleq2s 2908 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝐷𝑛 ∈ ω)
57 nnord 7581 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → Ord 𝑛)
58 ordtr1 6209 . . . . . . . . . . . . . . . . . . . . 21 (Ord 𝑛 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐷 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
6059imp 410 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)) → 𝑘𝑛)
6154, 60sylbi 220 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑛𝑛𝐷𝑘𝑗) → 𝑘𝑛)
6250, 61syl3an3 1162 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘𝑛)
63 rsp 3170 . . . . . . . . . . . . . . . . . 18 (∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃) → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6425, 63sylbi 220 . . . . . . . . . . . . . . . . 17 (𝜏 → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6562, 64mpan9 510 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
6648, 65mpd 15 . . . . . . . . . . . . . . 15 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
6745, 66sylbi 220 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → [𝑘 / 𝑗]𝜃)
6867anim1i 617 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
69 bnj252 32149 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
7068, 69sylibr 237 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′))
71 bnj446 32163 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72 bnj594.16 . . . . . . . . . . . . . 14 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
73 pm3.35 802 . . . . . . . . . . . . . 14 (((𝑛𝐷𝜒𝜒′) ∧ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))) → (𝑓𝑘) = (𝑔𝑘))
7472, 73sylan2b 596 . . . . . . . . . . . . 13 (((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓𝑘) = (𝑔𝑘))
7571, 74sylbi 220 . . . . . . . . . . . 12 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))
76 iuneq1 4901 . . . . . . . . . . . 12 ((𝑓𝑘) = (𝑔𝑘) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
7770, 75, 763syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
78 bnj658 32198 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘))
791simp3bi 1144 . . . . . . . . . . . . . 14 (𝜒𝜓)
805simp3bi 1144 . . . . . . . . . . . . . 14 (𝜒′𝜓′)
8179, 80bnj240 32145 . . . . . . . . . . . . 13 ((𝑛𝐷𝜒𝜒′) → (𝜓𝜓′))
8278, 81anim12i 615 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)))
83 simpl 486 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓)
8483anim2i 619 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓))
85 simp3 1135 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
8685anim1i 617 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘𝜓))
87 simpl1 1188 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → 𝑗𝑛)
88 df-3an 1086 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘))
8988biancomi 466 . . . . . . . . . . . . . . . 16 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
90 elnn 7583 . . . . . . . . . . . . . . . . 17 ((𝑘𝑗𝑗 ∈ ω) → 𝑘 ∈ ω)
9150, 33, 90syl2an 598 . . . . . . . . . . . . . . . 16 ((𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)) → 𝑘 ∈ ω)
9289, 91sylbi 220 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 ∈ ω)
93 bnj594.2 . . . . . . . . . . . . . . . . 17 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
9493bnj589 32357 . . . . . . . . . . . . . . . 16 (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑓‘suc 𝑘) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9594bnj590 32358 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))))
9692, 95mpan9 510 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9787, 96mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9886, 97syldan 594 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9982, 84, 983syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
100 simpr 488 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓′)
101100anim2i 619 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′))
10285anim1i 617 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘𝜓′))
103 simpl1 1188 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → 𝑗𝑛)
104 bnj594.10 . . . . . . . . . . . . . . . . 17 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
105104bnj589 32357 . . . . . . . . . . . . . . . 16 (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑔‘suc 𝑘) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
106105bnj590 32358 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓′) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))))
10792, 106mpan9 510 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
108103, 107mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
109102, 108syldan 594 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11082, 101, 1093syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11177, 99, 1103eqtr4d 2843 . . . . . . . . . 10 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗))
112111ex 416 . . . . . . . . 9 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11344, 112syl 17 . . . . . . . 8 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11440, 113bnj593 32192 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
115 bnj258 32154 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷))
116 19.9v 1988 . . . . . . 7 (∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)) ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
117114, 115, 1163imtr3i 294 . . . . . 6 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
118117expimpd 457 . . . . 5 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗)))
11923, 118syl5bir 246 . . . 4 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
120119, 16sylibr 237 . . 3 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → 𝜃)
1211203expib 1119 . 2 (𝑗 ≠ ∅ → ((𝑗𝑛𝜏) → 𝜃))
12218, 121pm2.61ine 3070 1 ((𝑗𝑛𝜏) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  [wsbc 3722   ∖ cdif 3880  ∅c0 4246  {csn 4528  ∪ ciun 4885   class class class wbr 5034   E cep 5433  Ord word 6165  suc csuc 6168   Fn wfn 6327  ‘cfv 6332  ωcom 7573   ∧ w-bnj17 32132   predc-bnj14 32134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-tr 5141  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fv 6340  df-om 7574  df-bnj17 32133 This theorem is referenced by:  bnj580  32361
 Copyright terms: Public domain W3C validator