Metamath Proof Explorer

Theorem bnj1118

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 bnj1118.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj1118.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj1118.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
bnj1118.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj1118.18 ⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
bnj1118.19 ⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
bnj1118.26 ⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
Assertion bnj1118 ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1118.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj1118.3 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
3 bnj1118.5 ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
4 bnj1118.7 ⊢ 𝐷 = ( ω ∖ { ∅ } )
5 bnj1118.18 ⊢ ( 𝜎 ↔ ( ( 𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖 ) → 𝜂′ ) )
6 bnj1118.19 ⊢ ( 𝜑0 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓 ) )
7 bnj1118.26 ⊢ ( 𝜂′ ↔ ( ( 𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
8 2 4 5 6 7 bnj1110 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
9 ancl ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) ) )
10 8 9 bnj101 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) )
11 simpr2 ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝑖 = suc 𝑗 )
12 2 bnj1254 ⊢ ( 𝜒 → 𝜓 )
13 12 3ad2ant3 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → 𝜓 )
14 13 ad2antrl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝜓 )
15 14 adantr ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝜓 )
16 2 bnj1232 ⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
17 16 3ad2ant3 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → 𝑛 ∈ 𝐷 )
18 17 ad2antrl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → 𝑛 ∈ 𝐷 )
19 18 adantr ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝑛 ∈ 𝐷 )
20 simpr1 ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝑗 ∈ 𝑛 )
21 4 bnj923 ⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
22 21 anim1i ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑗 ∈ 𝑛 ) → ( 𝑛 ∈ ω ∧ 𝑗 ∈ 𝑛 ) )
23 22 ancomd ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑗 ∈ 𝑛 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω ) )
24 19 20 23 syl2anc ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω ) )
25 elnn ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑗 ∈ ω )
26 24 25 syl ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝑗 ∈ ω )
27 6 bnj1232 ⊢ ( 𝜑0 → 𝑖 ∈ 𝑛 )
28 27 adantl ⊢ ( ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) → 𝑖 ∈ 𝑛 )
29 28 ad2antlr ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → 𝑖 ∈ 𝑛 )
30 11 15 26 29 bnj951 ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( 𝑖 = suc 𝑗 ∧ 𝜓 ∧ 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) )
31 3 simp2bi ⊢ ( 𝜏 → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )
32 31 3ad2ant2 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )
33 32 ad2antrl ⊢ ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )
34 simp3 ⊢ ( ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 )
35 33 34 anim12i ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) )
36 bnj256 ⊢ ( ( 𝑖 = suc 𝑗 ∧ 𝜓 ∧ 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) ↔ ( ( 𝑖 = suc 𝑗 ∧ 𝜓 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) ) )
37 1 bnj1112 ⊢ ( 𝜓 ↔ ∀ 𝑗 ( ( 𝑗 ∈ ω ∧ suc 𝑗 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
38 37 biimpi ⊢ ( 𝜓 → ∀ 𝑗 ( ( 𝑗 ∈ ω ∧ suc 𝑗 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
39 38 19.21bi ⊢ ( 𝜓 → ( ( 𝑗 ∈ ω ∧ suc 𝑗 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
40 eleq1 ⊢ ( 𝑖 = suc 𝑗 → ( 𝑖 ∈ 𝑛 ↔ suc 𝑗 ∈ 𝑛 ) )
41 40 anbi2d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) ↔ ( 𝑗 ∈ ω ∧ suc 𝑗 ∈ 𝑛 ) ) )
42 fveqeq2 ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
43 41 42 imbi12d ⊢ ( 𝑖 = suc 𝑗 → ( ( ( 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑗 ∈ ω ∧ suc 𝑗 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑗 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
44 39 43 syl5ibr ⊢ ( 𝑖 = suc 𝑗 → ( 𝜓 → ( ( 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
45 44 imp31 ⊢ ( ( ( 𝑖 = suc 𝑗 ∧ 𝜓 ) ∧ ( 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) ) → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
46 36 45 sylbi ⊢ ( ( 𝑖 = suc 𝑗 ∧ 𝜓 ∧ 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
47 df-bnj19 ⊢ ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∀ 𝑦 ∈ 𝐵 pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
48 ssralv ⊢ ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
49 47 48 syl5bi ⊢ ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 → ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
50 49 impcom ⊢ ( ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
51 iunss ⊢ ( ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 ↔ ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
52 50 51 sylibr ⊢ ( ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
53 sseq1 ⊢ ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) → ( ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 ↔ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) )
54 53 biimpar ⊢ ( ( ( 𝑓 ‘ 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∧ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑗 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
55 46 52 54 syl2an ⊢ ( ( ( 𝑖 = suc 𝑗 ∧ 𝜓 ∧ 𝑗 ∈ ω ∧ 𝑖 ∈ 𝑛 ) ∧ ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
56 30 35 55 syl2anc ⊢ ( ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) ∧ ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ ( 𝑓 ‘ 𝑗 ) ⊆ 𝐵 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )
57 10 56 bnj1023 ⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ ( ( 𝜃 ∧ 𝜏 ∧ 𝜒 ) ∧ 𝜑0 ) ) → ( 𝑓 ‘ 𝑖 ) ⊆ 𝐵 )