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

Metamath Proof Explorer

Theorem bnj1110

Description: Technical lemma for bnj69 . 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 bnj1110.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj1110.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj1110.18 ⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
bnj1110.19 ⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
bnj1110.26 ⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
Assertion bnj1110 ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 bnj1110.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2 bnj1110.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
3 bnj1110.18 ⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
4 bnj1110.19 ⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
5 bnj1110.26 ⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
6 2 bnj1098 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
7 bnj219 ⊢ ( 𝑖 = suc 𝑗 → 𝑗 E 𝑖 )
8 7 adantl ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) → 𝑗 E 𝑖 )
9 8 ancli ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ∧ 𝑗 E 𝑖 ) )
10 df-3an ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) ∧ 𝑗 E 𝑖 ) )
11 9 10 sylibr ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) )
12 6 11 bnj1023 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) )
13 1 bnj1232 ⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
14 13 3ad2ant3 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → 𝑛 ∈ 𝐷 )
15 4 bnj1232 ⊢ ( 𝜑0 → 𝑖 ∈ 𝑛 )
16 14 15 anim12ci ⊢ ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) )
17 16 anim2i ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) )
18 3anass ⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( 𝑖 ≠ ∅ ∧ ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) )
19 17 18 sylibr ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) )
20 12 19 bnj1101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) )
21 3simpb ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) )
22 4 bnj1235 ⊢ ( 𝜑0 → 𝜎 )
23 22 ad2antll ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝜎 )
24 23 3 sylib ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
25 21 24 syl5 ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
26 25 a2i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝜂′ ) )
27 pm3.43 ⊢ ( ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ) ∧ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝜂′ ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) )
28 26 27 mpdan ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) )
29 20 28 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) )
30 4 bnj1247 ⊢ ( 𝜑0 → 𝑓 ∈ 𝐾 )
31 30 ad2antll ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝑓 ∈ 𝐾 )
32 pm3.43i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝑓 ∈ 𝐾 ) → ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) ) )
33 31 32 ax-mp ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) )
34 29 33 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) )
35 fndm ⊢ ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
36 1 35 bnj770 ⊢ ( 𝜒 → dom 𝑓 = 𝑛 )
37 36 3ad2ant3 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → dom 𝑓 = 𝑛 )
38 37 ad2antrl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → dom 𝑓 = 𝑛 )
39 38 eleq2d ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) )
40 pm3.43i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ) → ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) ) ) )
41 39 40 ax-mp ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) ) )
42 34 41 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) )
43 bnj268 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ 𝑓 ∈ 𝐾 ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ↔ ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) )
44 bnj251 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ 𝑓 ∈ 𝐾 ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ↔ ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) )
45 43 44 bitr3i ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) ↔ ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) )
46 45 imbi2i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) ) ↔ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) ) )
47 46 exbii ⊢ ( ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) ) ↔ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑓 ∈ 𝐾 ∧ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ) ) ) )
48 42 47 mpbir ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) )
49 simp1 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) → 𝑗 ∈ 𝑛 )
50 49 bnj706 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → 𝑗 ∈ 𝑛 )
51 simp2 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) → 𝑖 = suc 𝑗 )
52 51 bnj706 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → 𝑖 = suc 𝑗 )
53 bnj258 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) ↔ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝜂′ ) ∧ 𝑓 ∈ 𝐾 ) )
54 53 simprbi ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → 𝑓 ∈ 𝐾 )
55 bnj642 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) )
56 50 55 mpbird ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → 𝑗 ∈ dom 𝑓 )
57 bnj645 ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → 𝜂′ )
58 57 5 sylib ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
59 54 56 58 mp2and ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 )
60 50 52 59 3jca ⊢ ( ( ( 𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛 ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖 ) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′ ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
61 48 60 bnj1023 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )