Metamath Proof Explorer

Theorem bnj570

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 bnj570.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj570.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
bnj570.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
bnj570.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
bnj570.24 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
bnj570.26 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
bnj570.40 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
bnj570.30 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
Assertion bnj570 ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )

Proof

Step Hyp Ref Expression
1 bnj570.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
2 bnj570.17 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
3 bnj570.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
4 bnj570.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
5 bnj570.24 ⊢ 𝐾 = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
6 bnj570.26 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , 𝐶 ⟩ } )
7 bnj570.40 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → 𝐺 Fn 𝑛 )
8 bnj570.30 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
9 bnj251 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) ↔ ( 𝑅 FrSe 𝐴 ∧ ( 𝜏 ∧ ( 𝜂 ∧ 𝜌 ) ) ) )
10 2 simp3bi ⊢ ( 𝜏 → 𝜓′ )
11 4 simp1bi ⊢ ( 𝜌 → 𝑖 ∈ ω )
12 11 adantl ⊢ ( ( 𝜂 ∧ 𝜌 ) → 𝑖 ∈ ω )
13 3 4 bnj563 ⊢ ( ( 𝜂 ∧ 𝜌 ) → suc 𝑖 ∈ 𝑚 )
14 12 13 jca ⊢ ( ( 𝜂 ∧ 𝜌 ) → ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑚 ) )
15 8 bnj946 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
16 sp ⊢ ( ∀ 𝑖 ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
17 15 16 sylbi ⊢ ( 𝜓′ → ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
18 17 imp32 ⊢ ( ( 𝜓′ ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑚 ) ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
19 10 14 18 syl2an ⊢ ( ( 𝜏 ∧ ( 𝜂 ∧ 𝜌 ) ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
20 9 19 simplbiim ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
21 7 fnfund ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ) → Fun 𝐺 )
22 21 bnj721 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → Fun 𝐺 )
23 6 bnj931 ⊢ 𝑓 ⊆ 𝐺
24 23 a1i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → 𝑓 ⊆ 𝐺 )
25 bnj667 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝜏 ∧ 𝜂 ∧ 𝜌 ) )
26 2 bnj564 ⊢ ( 𝜏 → dom 𝑓 = 𝑚 )
27 eleq2 ⊢ ( dom 𝑓 = 𝑚 → ( suc 𝑖 ∈ dom 𝑓 ↔ suc 𝑖 ∈ 𝑚 ) )
28 27 biimpar ⊢ ( ( dom 𝑓 = 𝑚 ∧ suc 𝑖 ∈ 𝑚 ) → suc 𝑖 ∈ dom 𝑓 )
29 26 13 28 syl2an ⊢ ( ( 𝜏 ∧ ( 𝜂 ∧ 𝜌 ) ) → suc 𝑖 ∈ dom 𝑓 )
30 29 3impb ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜌 ) → suc 𝑖 ∈ dom 𝑓 )
31 25 30 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → suc 𝑖 ∈ dom 𝑓 )
32 22 24 31 bnj1502 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) )
33 2 simp1bi ⊢ ( 𝜏 → 𝑓 Fn 𝑚 )
34 bnj252 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( 𝑚 ∈ 𝐷 ∧ ( 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ) )
35 34 simplbi ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) → 𝑚 ∈ 𝐷 )
36 3 35 sylbi ⊢ ( 𝜂 → 𝑚 ∈ 𝐷 )
37 eldifi ⊢ ( 𝑚 ∈ ( ω ∖ { ∅ } ) → 𝑚 ∈ ω )
38 37 1 eleq2s ⊢ ( 𝑚 ∈ 𝐷 → 𝑚 ∈ ω )
39 nnord ⊢ ( 𝑚 ∈ ω → Ord 𝑚 )
40 36 38 39 3syl ⊢ ( 𝜂 → Ord 𝑚 )
41 40 adantr ⊢ ( ( 𝜂 ∧ 𝜌 ) → Ord 𝑚 )
42 41 13 jca ⊢ ( ( 𝜂 ∧ 𝜌 ) → ( Ord 𝑚 ∧ suc 𝑖 ∈ 𝑚 ) )
43 33 42 anim12i ⊢ ( ( 𝜏 ∧ ( 𝜂 ∧ 𝜌 ) ) → ( 𝑓 Fn 𝑚 ∧ ( Ord 𝑚 ∧ suc 𝑖 ∈ 𝑚 ) ) )
44 fndm ⊢ ( 𝑓 Fn 𝑚 → dom 𝑓 = 𝑚 )
45 elelsuc ⊢ ( suc 𝑖 ∈ 𝑚 → suc 𝑖 ∈ suc 𝑚 )
46 ordsucelsuc ⊢ ( Ord 𝑚 → ( 𝑖 ∈ 𝑚 ↔ suc 𝑖 ∈ suc 𝑚 ) )
47 46 biimpar ⊢ ( ( Ord 𝑚 ∧ suc 𝑖 ∈ suc 𝑚 ) → 𝑖 ∈ 𝑚 )
48 45 47 sylan2 ⊢ ( ( Ord 𝑚 ∧ suc 𝑖 ∈ 𝑚 ) → 𝑖 ∈ 𝑚 )
49 44 48 anim12i ⊢ ( ( 𝑓 Fn 𝑚 ∧ ( Ord 𝑚 ∧ suc 𝑖 ∈ 𝑚 ) ) → ( dom 𝑓 = 𝑚 ∧ 𝑖 ∈ 𝑚 ) )
50 eleq2 ⊢ ( dom 𝑓 = 𝑚 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑚 ) )
51 50 biimpar ⊢ ( ( dom 𝑓 = 𝑚 ∧ 𝑖 ∈ 𝑚 ) → 𝑖 ∈ dom 𝑓 )
52 43 49 51 3syl ⊢ ( ( 𝜏 ∧ ( 𝜂 ∧ 𝜌 ) ) → 𝑖 ∈ dom 𝑓 )
53 52 3impb ⊢ ( ( 𝜏 ∧ 𝜂 ∧ 𝜌 ) → 𝑖 ∈ dom 𝑓 )
54 25 53 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → 𝑖 ∈ dom 𝑓 )
55 22 24 54 bnj1502 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
56 55 iuneq1d ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
57 20 32 56 3eqtr4d ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
58 57 5 eqtr4di ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌 ) → ( 𝐺 ‘ suc 𝑖 ) = 𝐾 )