Theorem bnj151

Description: Technical lemma for bnj153 . 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	bnj151.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj151.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj151.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj151.4	⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
	bnj151.5	⊢ ( 𝜏 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜃 ) )
	bnj151.6	⊢ ( 𝜁 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
	bnj151.7	⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
	bnj151.8	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
	bnj151.9	⊢ ( 𝜃′ ↔ [ 1o / 𝑛 ] 𝜃 )
	bnj151.10	⊢ ( 𝜃0 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
	bnj151.11	⊢ ( 𝜃1 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
	bnj151.12	⊢ ( 𝜁′ ↔ [ 1o / 𝑛 ] 𝜁 )
	bnj151.13	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
	bnj151.14	⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
	bnj151.15	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
	bnj151.16	⊢ ( 𝜁″ ↔ [ 𝐹 / 𝑓 ] 𝜁′ )
	bnj151.17	⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj151.18	⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
	bnj151.19	⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
	bnj151.20	⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
Assertion	bnj151	⊢ ( 𝑛 = 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj151.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj151.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj151.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj151.4	⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
5		bnj151.5	⊢ ( 𝜏 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜃 ) )
6		bnj151.6	⊢ ( 𝜁 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
7		bnj151.7	⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
8		bnj151.8	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
9		bnj151.9	⊢ ( 𝜃′ ↔ [ 1o / 𝑛 ] 𝜃 )
10		bnj151.10	⊢ ( 𝜃0 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
11		bnj151.11	⊢ ( 𝜃1 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
12		bnj151.12	⊢ ( 𝜁′ ↔ [ 1o / 𝑛 ] 𝜁 )
13		bnj151.13	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
14		bnj151.14	⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
15		bnj151.15	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
16		bnj151.16	⊢ ( 𝜁″ ↔ [ 𝐹 / 𝑓 ] 𝜁′ )
17		bnj151.17	⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
18		bnj151.18	⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
19		bnj151.19	⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
20		bnj151.20	⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
21	1 2 6 7 8 10 12 13 14 15 16	bnj150	⊢ 𝜃0
22	21 10	mpbi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
23	1 7	bnj118	⊢ ( 𝜑′ ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
24	11 17 18 19 20 23	bnj149	⊢ 𝜃1
25	24 11	mpbi	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
26		df-eu	⊢ ( ∃! 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ∧ ∃* 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
27	22 25 26	sylanbrc	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
28	4 7 8 9	bnj130	⊢ ( 𝜃′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
29	27 28	mpbir	⊢ 𝜃′
30		sbceq1a	⊢ ( 𝑛 = 1o → ( 𝜃 ↔ [ 1o / 𝑛 ] 𝜃 ) )
31	30 9	bitr4di	⊢ ( 𝑛 = 1o → ( 𝜃 ↔ 𝜃′ ) )
32	29 31	mpbiri	⊢ ( 𝑛 = 1o → 𝜃 )
33	32	a1d	⊢ ( 𝑛 = 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )