Theorem bnj535

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

Proof

Step	Hyp	Ref	Expression
1		bnj535.1	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj535.2	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑚 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj535.3	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
4		bnj535.4	⊢ ( 𝜏 ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚 ) )
5		bnj422	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) ↔ ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ∧ 𝑅 FrSe 𝐴 ∧ 𝜏 ) )
6		bnj251	⊢ ( ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ∧ 𝑅 FrSe 𝐴 ∧ 𝜏 ) ↔ ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) ) )
7	5 6	bitri	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) ↔ ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) ) )
8		fvex	⊢ ( 𝑓 ‘ 𝑝 ) ∈ V
9	1 2 4	bnj518	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
10		iunexg	⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∈ V ∧ ∀ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
11	8 9 10	sylancr	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V )
12		vex	⊢ 𝑚 ∈ V
13	12	bnj519	⊢ ( ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V → Fun { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
14	11 13	syl	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → Fun { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
15		dmsnopg	⊢ ( ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∈ V → dom { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } = { 𝑚 } )
16	11 15	syl	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → dom { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } = { 𝑚 } )
17	14 16	bnj1422	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) → { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } Fn { 𝑚 } )
18		bnj521	⊢ ( 𝑚 ∩ { 𝑚 } ) = ∅
19		fnun	⊢ ( ( ( 𝑓 Fn 𝑚 ∧ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } Fn { 𝑚 } ) ∧ ( 𝑚 ∩ { 𝑚 } ) = ∅ ) → ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) Fn ( 𝑚 ∪ { 𝑚 } ) )
20	18 19	mpan2	⊢ ( ( 𝑓 Fn 𝑚 ∧ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } Fn { 𝑚 } ) → ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) Fn ( 𝑚 ∪ { 𝑚 } ) )
21	17 20	sylan2	⊢ ( ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) → ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) Fn ( 𝑚 ∪ { 𝑚 } ) )
22	3	fneq1i	⊢ ( 𝐺 Fn ( 𝑚 ∪ { 𝑚 } ) ↔ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) Fn ( 𝑚 ∪ { 𝑚 } ) )
23	21 22	sylibr	⊢ ( ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) → 𝐺 Fn ( 𝑚 ∪ { 𝑚 } ) )
24		fneq2	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) → ( 𝐺 Fn 𝑛 ↔ 𝐺 Fn ( 𝑚 ∪ { 𝑚 } ) ) )
25	23 24	syl5ibr	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) → ( ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) → 𝐺 Fn 𝑛 ) )
26	25	imp	⊢ ( ( 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ ( 𝑓 Fn 𝑚 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝜏 ) ) ) → 𝐺 Fn 𝑛 )
27	7 26	sylbi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = ( 𝑚 ∪ { 𝑚 } ) ∧ 𝑓 Fn 𝑚 ) → 𝐺 Fn 𝑛 )