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 𝑗 ∧ ( 𝑓𝑗 ) ⊆ 𝐵 ) )