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

Metamath Proof Explorer

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