This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )