Theorem bnj601

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	bnj601.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj601.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj601.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj601.4	⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
	bnj601.5	⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
Assertion	bnj601	⊢ ( 𝑛 ≠ 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜃 ) → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj601.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj601.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj601.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj601.4	⊢ ( 𝜒 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
5		bnj601.5	⊢ ( 𝜃 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜒 ) )
6		biid	⊢ ( [ 𝑚 / 𝑛 ] 𝜑 ↔ [ 𝑚 / 𝑛 ] 𝜑 )
7		biid	⊢ ( [ 𝑚 / 𝑛 ] 𝜓 ↔ [ 𝑚 / 𝑛 ] 𝜓 )
8		biid	⊢ ( [ 𝑚 / 𝑛 ] 𝜒 ↔ [ 𝑚 / 𝑛 ] 𝜒 )
9		bnj602	⊢ ( 𝑦 = 𝑧 → pred ( 𝑦 , 𝐴 , 𝑅 ) = pred ( 𝑧 , 𝐴 , 𝑅 ) )
10	9	cbviunv	⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 )
11	10	opeq2i	⊢ ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ = ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩
12	11	sneqi	⊢ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } = { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ }
13	12	uneq2i	⊢ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } )
14		dfsbcq	⊢ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) → ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜑 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜑 ) )
15	13 14	ax-mp	⊢ ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜑 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜑 )
16		dfsbcq	⊢ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) → ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜓 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜓 ) )
17	13 16	ax-mp	⊢ ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜓 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜓 )
18		dfsbcq	⊢ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) → ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜒 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜒 ) )
19	13 18	ax-mp	⊢ ( [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜒 ↔ [ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) / 𝑓 ] 𝜒 )
20	13	eqcomi	⊢ ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⟩ } )
21		biid	⊢ ( ( 𝑓 Fn 𝑚 ∧ [ 𝑚 / 𝑛 ] 𝜑 ∧ [ 𝑚 / 𝑛 ] 𝜓 ) ↔ ( 𝑓 Fn 𝑚 ∧ [ 𝑚 / 𝑛 ] 𝜑 ∧ [ 𝑚 / 𝑛 ] 𝜓 ) )
22		biid	⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚 ) )
23		biid	⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
24		biid	⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖 ) )
25		biid	⊢ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
26		eqid	⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
27		eqid	⊢ ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
28		eqid	⊢ ∪ 𝑦 ∈ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 )
29		eqid	⊢ ∪ 𝑦 ∈ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( ( 𝑓 ∪ { ⟨ 𝑚 , ∪ 𝑧 ∈ ( 𝑓 ‘ 𝑝 ) pred ( 𝑧 , 𝐴 , 𝑅 ) ⟩ } ) ‘ 𝑝 ) pred ( 𝑦 , 𝐴 , 𝑅 )
30	1 2 3 4 5 6 7 8 15 17 19 20 21 22 23 24 25 26 27 28 29 20	bnj600	⊢ ( 𝑛 ≠ 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜃 ) → 𝜒 ) )