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 31108
Description: Technical lemma for bnj852 31117. 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 1097 . . . . . . . 8 (𝜒𝜑)
3 bnj594.1 . . . . . . . 8 (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
42, 3sylib 208 . . . . . . 7 (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5 bnj594.11 . . . . . . . . 9 (𝜒′ ↔ (𝑔 Fn 𝑛𝜑′𝜓′))
65simp2bi 1097 . . . . . . . 8 (𝜒′𝜑′)
7 bnj594.9 . . . . . . . 8 (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
86, 7sylib 208 . . . . . . 7 (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9 eqtr3 2672 . . . . . . 7 (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
104, 8, 9syl2an 493 . . . . . 6 ((𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11103adant1 1099 . . . . 5 ((𝑛𝐷𝜒𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12 fveq2 6229 . . . . . 6 (𝑗 = ∅ → (𝑓𝑗) = (𝑓‘∅))
13 fveq2 6229 . . . . . 6 (𝑗 = ∅ → (𝑔𝑗) = (𝑔‘∅))
1412, 13eqeq12d 2666 . . . . 5 (𝑗 = ∅ → ((𝑓𝑗) = (𝑔𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
1511, 14syl5ibr 236 . . . 4 (𝑗 = ∅ → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
16 bnj594.15 . . . 4 (𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
1715, 16sylibr 224 . . 3 (𝑗 = ∅ → 𝜃)
1817a1d 25 . 2 (𝑗 = ∅ → ((𝑗𝑛𝜏) → 𝜃))
19 bnj253 30898 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′))
20 bnj252 30897 . . . . . 6 ((𝑛𝐷𝑛𝐷𝜒𝜒′) ↔ (𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)))
21 anidm 677 . . . . . . 7 ((𝑛𝐷𝑛𝐷) ↔ 𝑛𝐷)
22213anbi1i 1272 . . . . . 6 (((𝑛𝐷𝑛𝐷) ∧ 𝜒𝜒′) ↔ (𝑛𝐷𝜒𝜒′))
2319, 20, 223bitr3i 290 . . . . 5 ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) ↔ (𝑛𝐷𝜒𝜒′))
24 df-bnj17 30881 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
25 bnj594.17 . . . . . . . . . . . 12 (𝜏 ↔ ∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
2625bnj1095 30978 . . . . . . . . . . 11 (𝜏 → ∀𝑘𝜏)
2726bnj1352 31024 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ∧ 𝜏))
2824, 27hbxfrbi 1792 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏))
29 bnj170 30892 . . . . . . . . . . . 12 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅))
30 bnj594.7 . . . . . . . . . . . . . . 15 𝐷 = (ω ∖ {∅})
3130bnj923 30964 . . . . . . . . . . . . . 14 (𝑛𝐷𝑛 ∈ ω)
32 elnn 7117 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛 ∈ ω) → 𝑗 ∈ ω)
3331, 32sylan2 490 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷) → 𝑗 ∈ ω)
3433anim1i 591 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
3529, 34sylbi 207 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36 nnsuc 7124 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37 rexex 3031 . . . . . . . . . . 11 (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
3835, 36, 373syl 18 . . . . . . . . . 10 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷) → ∃𝑘 𝑗 = suc 𝑘)
3938bnj721 30953 . . . . . . . . 9 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘 𝑗 = suc 𝑘)
4028, 39bnj596 30942 . . . . . . . 8 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
41 bnj667 30948 . . . . . . . . . . 11 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → (𝑗𝑛𝑛𝐷𝜏))
4241anim1i 591 . . . . . . . . . 10 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
43 bnj258 30902 . . . . . . . . . 10 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘))
4442, 43sylibr 224 . . . . . . . . 9 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏))
45 df-bnj17 30881 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ↔ ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏))
46 bnj219 30927 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘 E 𝑗)
47463ad2ant3 1104 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 E 𝑗)
4847adantr 480 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
5049bnj216 30926 . . . . . . . . . . . . . . . . . 18 (𝑗 = suc 𝑘𝑘𝑗)
51 df-3an 1056 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ ((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷))
52 3anrot 1060 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝑗𝑗𝑛𝑛𝐷) ↔ (𝑗𝑛𝑛𝐷𝑘𝑗))
53 ancom 465 . . . . . . . . . . . . . . . . . . . 20 (((𝑘𝑗𝑗𝑛) ∧ 𝑛𝐷) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
5451, 52, 533bitr3i 290 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑛𝑛𝐷𝑘𝑗) ↔ (𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)))
55 eldifi 3765 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
5655, 30eleq2s 2748 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝐷𝑛 ∈ ω)
57 nnord 7115 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → Ord 𝑛)
58 ordtr1 5805 . . . . . . . . . . . . . . . . . . . . 21 (Ord 𝑛 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐷 → ((𝑘𝑗𝑗𝑛) → 𝑘𝑛))
6059imp 444 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝐷 ∧ (𝑘𝑗𝑗𝑛)) → 𝑘𝑛)
6154, 60sylbi 207 . . . . . . . . . . . . . . . . . 18 ((𝑗𝑛𝑛𝐷𝑘𝑗) → 𝑘𝑛)
6250, 61syl3an3 1401 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘𝑛)
63 rsp 2958 . . . . . . . . . . . . . . . . . 18 (∀𝑘𝑛 (𝑘 E 𝑗[𝑘 / 𝑗]𝜃) → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6425, 63sylbi 207 . . . . . . . . . . . . . . . . 17 (𝜏 → (𝑘𝑛 → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃)))
6562, 64mpan9 485 . . . . . . . . . . . . . . . 16 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗[𝑘 / 𝑗]𝜃))
6648, 65mpd 15 . . . . . . . . . . . . . . 15 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
6745, 66sylbi 207 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → [𝑘 / 𝑗]𝜃)
6867anim1i 591 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
69 bnj252 30897 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛𝐷𝜒𝜒′)))
7068, 69sylibr 224 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′))
71 bnj446 30911 . . . . . . . . . . . . 13 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) ↔ ((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72 bnj594.16 . . . . . . . . . . . . . 14 ([𝑘 / 𝑗]𝜃 ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘)))
73 pm3.35 610 . . . . . . . . . . . . . 14 (((𝑛𝐷𝜒𝜒′) ∧ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))) → (𝑓𝑘) = (𝑔𝑘))
7472, 73sylan2b 491 . . . . . . . . . . . . 13 (((𝑛𝐷𝜒𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓𝑘) = (𝑔𝑘))
7571, 74sylbi 207 . . . . . . . . . . . 12 (([𝑘 / 𝑗]𝜃𝑛𝐷𝜒𝜒′) → (𝑓𝑘) = (𝑔𝑘))
76 iuneq1 4566 . . . . . . . . . . . 12 ((𝑓𝑘) = (𝑔𝑘) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
7770, 75, 763syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
78 bnj658 30947 . . . . . . . . . . . . 13 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → (𝑗𝑛𝑛𝐷𝑗 = suc 𝑘))
791simp3bi 1098 . . . . . . . . . . . . . 14 (𝜒𝜓)
805simp3bi 1098 . . . . . . . . . . . . . 14 (𝜒′𝜓′)
8179, 80bnj240 30893 . . . . . . . . . . . . 13 ((𝑛𝐷𝜒𝜒′) → (𝜓𝜓′))
8278, 81anim12i 589 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)))
83 simpl 472 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓)
8483anim2i 592 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓))
85 simp3 1083 . . . . . . . . . . . . . 14 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
8685anim1i 591 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘𝜓))
87 simpl1 1084 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → 𝑗𝑛)
88 df-3an 1056 . . . . . . . . . . . . . . . . 17 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ ((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘))
89 ancom 465 . . . . . . . . . . . . . . . . 17 (((𝑗𝑛𝑛𝐷) ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
9088, 89bitri 264 . . . . . . . . . . . . . . . 16 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)))
91 elnn 7117 . . . . . . . . . . . . . . . . 17 ((𝑘𝑗𝑗 ∈ ω) → 𝑘 ∈ ω)
9250, 33, 91syl2an 493 . . . . . . . . . . . . . . . 16 ((𝑗 = suc 𝑘 ∧ (𝑗𝑛𝑛𝐷)) → 𝑘 ∈ ω)
9390, 92sylbi 207 . . . . . . . . . . . . . . 15 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) → 𝑘 ∈ ω)
94 bnj594.2 . . . . . . . . . . . . . . . . 17 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
9594bnj589 31105 . . . . . . . . . . . . . . . 16 (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑓‘suc 𝑘) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9695bnj590 31106 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))))
9793, 96mpan9 485 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑗𝑛 → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅)))
9887, 97mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
9986, 98syldan 486 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
10082, 84, 993syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = 𝑦 ∈ (𝑓𝑘) pred(𝑦, 𝐴, 𝑅))
101 simpr 476 . . . . . . . . . . . . 13 ((𝜓𝜓′) → 𝜓′)
102101anim2i 592 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝜓𝜓′)) → ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′))
10385anim1i 591 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘𝜓′))
104 simpl1 1084 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → 𝑗𝑛)
105 bnj594.10 . . . . . . . . . . . . . . . . 17 (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑔‘suc 𝑖) = 𝑦 ∈ (𝑔𝑖) pred(𝑦, 𝐴, 𝑅)))
106105bnj589 31105 . . . . . . . . . . . . . . . 16 (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘𝑛 → (𝑔‘suc 𝑘) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
107106bnj590 31106 . . . . . . . . . . . . . . 15 ((𝑗 = suc 𝑘𝜓′) → (𝑘 ∈ ω → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))))
10893, 107mpan9 485 . . . . . . . . . . . . . 14 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑗𝑛 → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅)))
109104, 108mpd 15 . . . . . . . . . . . . 13 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘𝜓′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
110103, 109syldan 486 . . . . . . . . . . . 12 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11182, 102, 1103syl 18 . . . . . . . . . . 11 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑔𝑗) = 𝑦 ∈ (𝑔𝑘) pred(𝑦, 𝐴, 𝑅))
11277, 100, 1113eqtr4d 2695 . . . . . . . . . 10 (((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗))
113112ex 449 . . . . . . . . 9 ((𝑗𝑛𝑛𝐷𝑗 = suc 𝑘𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11444, 113syl 17 . . . . . . . 8 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
11540, 114bnj593 30941 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) → ∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
116 bnj258 30902 . . . . . . 7 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝑛𝐷𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷))
117 19.9v 1953 . . . . . . 7 (∃𝑘((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)) ↔ ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
118115, 116, 1173imtr3i 280 . . . . . 6 (((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) ∧ 𝑛𝐷) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
119118expimpd 628 . . . . 5 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷 ∧ (𝑛𝐷𝜒𝜒′)) → (𝑓𝑗) = (𝑔𝑗)))
12023, 119syl5bir 233 . . . 4 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → ((𝑛𝐷𝜒𝜒′) → (𝑓𝑗) = (𝑔𝑗)))
121120, 16sylibr 224 . . 3 ((𝑗 ≠ ∅ ∧ 𝑗𝑛𝜏) → 𝜃)
1221213expib 1287 . 2 (𝑗 ≠ ∅ → ((𝑗𝑛𝜏) → 𝜃))
12318, 122pm2.61ine 2906 1 ((𝑗𝑛𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  [wsbc 3468  cdif 3604  c0 3948  {csn 4210   ciun 4552   class class class wbr 4685   E cep 5057  Ord word 5760  suc csuc 5763   Fn wfn 5921  cfv 5926  ωcom 7107  w-bnj17 30880   predc-bnj14 30882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-tr 4786  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fv 5934  df-om 7108  df-bnj17 30881
This theorem is referenced by:  bnj580  31109
  Copyright terms: Public domain W3C validator