This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj594

Description: Technical lemma for bnj852 . 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.)

Ref Expression
Hypotheses 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 bnj594 ( ( 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 bnj594.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj594.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj594.3 ⊢ ( 𝜒 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4 bnj594.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
5 bnj594.9 ⊢ ( 𝜑′ ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
6 bnj594.10 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
7 bnj594.11 ⊢ ( 𝜒′ ↔ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
8 bnj594.15 ⊢ ( 𝜃 ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
9 bnj594.16 ⊢ ( [ 𝑘 / 𝑗 ] 𝜃 ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) ) )
10 bnj594.17 ⊢ ( 𝜏 ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) )
11 3 simp2bi ⊢ ( 𝜒 → 𝜑 )
12 11 1 sylib ⊢ ( 𝜒 → ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
13 7 simp2bi ⊢ ( 𝜒′ → 𝜑′ )
14 13 5 sylib ⊢ ( 𝜒′ → ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
15 eqtr3 ⊢ ( ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) )
16 12 14 15 syl2an ⊢ ( ( 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) )
17 16 3adant1 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) )
18 fveq2 ⊢ ( 𝑗 = ∅ → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ ∅ ) )
19 fveq2 ⊢ ( 𝑗 = ∅ → ( 𝑔 ‘ 𝑗 ) = ( 𝑔 ‘ ∅ ) )
20 18 19 eqeq12d ⊢ ( 𝑗 = ∅ → ( ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ↔ ( 𝑓 ‘ ∅ ) = ( 𝑔 ‘ ∅ ) ) )
21 17 20 imbitrrid ⊢ ( 𝑗 = ∅ → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
22 21 8 sylibr ⊢ ( 𝑗 = ∅ → 𝜃 )
23 22 a1d ⊢ ( 𝑗 = ∅ → ( ( 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 ) )
24 bnj253 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜒 ∧ 𝜒′ ) )
25 bnj252 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) )
26 anidm ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ) ↔ 𝑛 ∈ 𝐷 )
27 26 3anbi1i ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜒 ∧ 𝜒′ ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) )
28 24 25 27 3bitr3i ⊢ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) )
29 df-bnj17 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ↔ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜏 ) )
30 10 bnj1095 ⊢ ( 𝜏 → ∀ 𝑘 𝜏 )
31 30 bnj1352 ⊢ ( ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜏 ) → ∀ 𝑘 ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝜏 ) )
32 29 31 hbxfrbi ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) → ∀ 𝑘 ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) )
33 bnj170 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑗 ≠ ∅ ) )
34 4 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
35 elnn ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑗 ∈ ω )
36 34 35 sylan2 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → 𝑗 ∈ ω )
37 36 anim1i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑗 ≠ ∅ ) → ( 𝑗 ∈ ω ∧ 𝑗 ≠ ∅ ) )
38 33 37 sylbi ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ ω ∧ 𝑗 ≠ ∅ ) )
39 nnsuc ⊢ ( ( 𝑗 ∈ ω ∧ 𝑗 ≠ ∅ ) → ∃ 𝑘 ∈ ω 𝑗 = suc 𝑘 )
40 rexex ⊢ ( ∃ 𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃ 𝑘 𝑗 = suc 𝑘 )
41 38 39 40 3syl ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑘 𝑗 = suc 𝑘 )
42 41 bnj721 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) → ∃ 𝑘 𝑗 = suc 𝑘 )
43 32 42 bnj596 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) → ∃ 𝑘 ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) )
44 bnj667 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) )
45 44 anim1i ⊢ ( ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) )
46 bnj258 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) )
47 45 46 sylibr ⊢ ( ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) )
48 df-bnj17 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜏 ) )
49 bnj219 ⊢ ( 𝑗 = suc 𝑘 → 𝑘 E 𝑗 )
50 49 3ad2ant3 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) → 𝑘 E 𝑗 )
51 50 adantr ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜏 ) → 𝑘 E 𝑗 )
52 vex ⊢ 𝑘 ∈ V
53 52 bnj216 ⊢ ( 𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗 )
54 df-3an ⊢ ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) ∧ 𝑛 ∈ 𝐷 ) )
55 3anrot ⊢ ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗 ) )
56 ancom ⊢ ( ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) ∧ 𝑛 ∈ 𝐷 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) ) )
57 54 55 56 3bitr3i ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) ) )
58 eldifi ⊢ ( 𝑛 ∈ ( ω ∖ { ∅ } ) → 𝑛 ∈ ω )
59 58 4 eleq2s ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
60 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
61 ordtr1 ⊢ ( Ord 𝑛 → ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) → 𝑘 ∈ 𝑛 ) )
62 59 60 61 3syl ⊢ ( 𝑛 ∈ 𝐷 → ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) → 𝑘 ∈ 𝑛 ) )
63 62 imp ⊢ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ) ) → 𝑘 ∈ 𝑛 )
64 57 63 sylbi ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗 ) → 𝑘 ∈ 𝑛 )
65 53 64 syl3an3 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) → 𝑘 ∈ 𝑛 )
66 rsp ⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) → ( 𝑘 ∈ 𝑛 → ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) ) )
67 10 66 sylbi ⊢ ( 𝜏 → ( 𝑘 ∈ 𝑛 → ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) ) )
68 65 67 mpan9 ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜏 ) → ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] 𝜃 ) )
69 51 68 mpd ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜏 ) → [ 𝑘 / 𝑗 ] 𝜃 )
70 48 69 sylbi ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) → [ 𝑘 / 𝑗 ] 𝜃 )
71 70 anim1i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( [ 𝑘 / 𝑗 ] 𝜃 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) )
72 bnj252 ⊢ ( ( [ 𝑘 / 𝑗 ] 𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ↔ ( [ 𝑘 / 𝑗 ] 𝜃 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) )
73 71 72 sylibr ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( [ 𝑘 / 𝑗 ] 𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) )
74 bnj446 ⊢ ( ( [ 𝑘 / 𝑗 ] 𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ∧ [ 𝑘 / 𝑗 ] 𝜃 ) )
75 pm3.35 ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ∧ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
76 9 75 sylan2b ⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ∧ [ 𝑘 / 𝑗 ] 𝜃 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
77 74 76 sylbi ⊢ ( ( [ 𝑘 / 𝑗 ] 𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
78 iuneq1 ⊢ ( ( 𝑓 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
79 73 77 78 3syl ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
80 bnj658 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) )
81 3 simp3bi ⊢ ( 𝜒 → 𝜓 )
82 7 simp3bi ⊢ ( 𝜒′ → 𝜓′ )
83 81 82 bnj240 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝜓 ∧ 𝜓′ ) )
84 80 83 anim12i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝜓 ∧ 𝜓′ ) ) )
85 simpl ⊢ ( ( 𝜓 ∧ 𝜓′ ) → 𝜓 )
86 85 anim2i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝜓 ∧ 𝜓′ ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓 ) )
87 simp3 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) → 𝑗 = suc 𝑘 )
88 87 anim1i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓 ) → ( 𝑗 = suc 𝑘 ∧ 𝜓 ) )
89 simpl1 ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓 ) ) → 𝑗 ∈ 𝑛 )
90 df-3an ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑗 = suc 𝑘 ) )
91 90 biancomi ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ↔ ( 𝑗 = suc 𝑘 ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) )
92 elnn ⊢ ( ( 𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω ) → 𝑘 ∈ ω )
93 53 36 92 syl2an ⊢ ( ( 𝑗 = suc 𝑘 ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → 𝑘 ∈ ω )
94 91 93 sylbi ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) → 𝑘 ∈ ω )
95 2 bnj589 ⊢ ( 𝜓 ↔ ∀ 𝑘 ∈ ω ( suc 𝑘 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑘 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
96 95 bnj590 ⊢ ( ( 𝑗 = suc 𝑘 ∧ 𝜓 ) → ( 𝑘 ∈ ω → ( 𝑗 ∈ 𝑛 → ( 𝑓 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
97 94 96 mpan9 ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓 ) ) → ( 𝑗 ∈ 𝑛 → ( 𝑓 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
98 89 97 mpd ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓 ) ) → ( 𝑓 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
99 88 98 syldan ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓 ) → ( 𝑓 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
100 84 86 99 3syl ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑓 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
101 simpr ⊢ ( ( 𝜓 ∧ 𝜓′ ) → 𝜓′ )
102 101 anim2i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝜓 ∧ 𝜓′ ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓′ ) )
103 87 anim1i ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓′ ) → ( 𝑗 = suc 𝑘 ∧ 𝜓′ ) )
104 simpl1 ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓′ ) ) → 𝑗 ∈ 𝑛 )
105 6 bnj589 ⊢ ( 𝜓′ ↔ ∀ 𝑘 ∈ ω ( suc 𝑘 ∈ 𝑛 → ( 𝑔 ‘ suc 𝑘 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
106 105 bnj590 ⊢ ( ( 𝑗 = suc 𝑘 ∧ 𝜓′ ) → ( 𝑘 ∈ ω → ( 𝑗 ∈ 𝑛 → ( 𝑔 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
107 94 106 mpan9 ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓′ ) ) → ( 𝑗 ∈ 𝑛 → ( 𝑔 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
108 104 107 mpd ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ ( 𝑗 = suc 𝑘 ∧ 𝜓′ ) ) → ( 𝑔 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
109 103 108 syldan ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ) ∧ 𝜓′ ) → ( 𝑔 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
110 84 102 109 3syl ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑔 ‘ 𝑗 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑘 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
111 79 100 110 3eqtr4d ⊢ ( ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) )
112 111 ex ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏 ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
113 47 112 syl ⊢ ( ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ∧ 𝑗 = suc 𝑘 ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
114 43 113 bnj593 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) → ∃ 𝑘 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
115 bnj258 ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏 ) ↔ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏 ) ∧ 𝑛 ∈ 𝐷 ) )
116 19.9v ⊢ ( ∃ 𝑘 ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
117 114 115 116 3imtr3i ⊢ ( ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏 ) ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
118 117 expimpd ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏 ) → ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
119 28 118 biimtrrid ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏 ) → ( ( 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′ ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
120 119 8 sylibr ⊢ ( ( 𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )
121 120 3expib ⊢ ( 𝑗 ≠ ∅ → ( ( 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 ) )
122 23 121 pm2.61ine ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝜏 ) → 𝜃 )