Metamath Proof Explorer

Theorem bnj546

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 bnj546.1 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj546.2 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
bnj546.3 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
bnj546.4 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj546.5 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
Assertion bnj546 ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step Hyp Ref Expression
1 bnj546.1 ⊢ 𝐷 = ( ω ∖ { ∅ } )
2 bnj546.2 ⊢ ( 𝜏 ↔ ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) )
3 bnj546.3 ⊢ ( 𝜎 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
4 bnj546.4 ⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
5 bnj546.5 ⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6 3simpc ⊢ ( ( 𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′ ) → ( 𝜑′ ∧ 𝜓′ ) )
7 2 6 sylbi ⊢ ( 𝜏 → ( 𝜑′ ∧ 𝜓′ ) )
8 1 bnj923 ⊢ ( 𝑚 ∈ 𝐷 → 𝑚 ∈ ω )
9 8 3ad2ant1 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) → 𝑚 ∈ ω )
10 simp3 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) → 𝑝 ∈ 𝑚 )
11 9 10 jca ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) → ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
12 3 11 sylbi ⊢ ( 𝜎 → ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
13 7 12 anim12i ⊢ ( ( 𝜏 ∧ 𝜎 ) → ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) )
14 bnj256 ⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ↔ ( ( 𝜑′ ∧ 𝜓′ ) ∧ ( 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) )
15 13 14 sylibr ⊢ ( ( 𝜏 ∧ 𝜎 ) → ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
16 15 anim2i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜏 ∧ 𝜎 ) ) → ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) )
17 16 3impb ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) )
18 biid ⊢ ( ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
19 4 5 18 bnj518 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
20 fvex ⊢ ( 𝑓 ‘ 𝑝 ) ∈ V
21 iunexg ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∈ V ∧ ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
22 20 21 mpan ⊢ ( ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
23 17 19 22 3syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )