Theorem bnj150

Description: Technical lemma for bnj151 . 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	bnj150.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj150.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj150.3	⊢ ( 𝜁 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
	bnj150.4	⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
	bnj150.5	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
	bnj150.6	⊢ ( 𝜃0 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
	bnj150.7	⊢ ( 𝜁′ ↔ [ 1o / 𝑛 ] 𝜁 )
	bnj150.8	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
	bnj150.9	⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
	bnj150.10	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
	bnj150.11	⊢ ( 𝜁″ ↔ [ 𝐹 / 𝑓 ] 𝜁′ )
Assertion	bnj150	⊢ 𝜃0

Proof

Step	Hyp	Ref	Expression
1		bnj150.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj150.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj150.3	⊢ ( 𝜁 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
4		bnj150.4	⊢ ( 𝜑′ ↔ [ 1o / 𝑛 ] 𝜑 )
5		bnj150.5	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
6		bnj150.6	⊢ ( 𝜃0 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
7		bnj150.7	⊢ ( 𝜁′ ↔ [ 1o / 𝑛 ] 𝜁 )
8		bnj150.8	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
9		bnj150.9	⊢ ( 𝜑″ ↔ [ 𝐹 / 𝑓 ] 𝜑′ )
10		bnj150.10	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
11		bnj150.11	⊢ ( 𝜁″ ↔ [ 𝐹 / 𝑓 ] 𝜁′ )
12	8	bnj95	⊢ 𝐹 ∈ V
13		sbceq1a	⊢ ( 𝑓 = 𝐹 → ( 𝜁′ ↔ [ 𝐹 / 𝑓 ] 𝜁′ ) )
14	13 11	bitr4di	⊢ ( 𝑓 = 𝐹 → ( 𝜁′ ↔ 𝜁″ ) )
15		0ex	⊢ ∅ ∈ V
16		bnj93	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
17		funsng	⊢ ( ( ∅ ∈ V ∧ pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V ) → Fun { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } )
18	15 16 17	sylancr	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Fun { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } )
19	8	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } )
20	18 19	sylibr	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Fun 𝐹 )
21	8	bnj96	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → dom 𝐹 = 1o )
22	20 21	bnj1422	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 Fn 1o )
23	8	bnj97	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
24	1 4 9 8	bnj125	⊢ ( 𝜑″ ↔ ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
25	23 24	sylibr	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝜑″ )
26	22 25	jca	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 Fn 1o ∧ 𝜑″ ) )
27		bnj98	⊢ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
28	2 5 10 8	bnj126	⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
29	27 28	mpbir	⊢ 𝜓″
30		df-3an	⊢ ( ( 𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″ ) ↔ ( ( 𝐹 Fn 1o ∧ 𝜑″ ) ∧ 𝜓″ ) )
31	26 29 30	sylanblrc	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″ ) )
32	3 7 4 5	bnj121	⊢ ( 𝜁′ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
33	8 9 10 11 32	bnj124	⊢ ( 𝜁″ ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″ ) ) )
34	31 33	mpbir	⊢ 𝜁″
35	12 14 34	ceqsexv2d	⊢ ∃ 𝑓 𝜁′
36		19.37v	⊢ ( ∃ 𝑓 ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
37	6 36	bitr4i	⊢ ( 𝜃0 ↔ ∃ 𝑓 ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ) )
38	37 32	bnj133	⊢ ( 𝜃0 ↔ ∃ 𝑓 𝜁′ )
39	35 38	mpbir	⊢ 𝜃0