Metamath Proof Explorer

Theorem bnj852

Description: Technical lemma for bnj69 . 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 bnj852.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj852.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj852.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion bnj852 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 bnj852.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj852.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj852.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 elisset ⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑥 𝑥 = 𝑋 )
5 4 adantl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 𝑥 = 𝑋 )
6 5 ancri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑥 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) )
7 6 bnj534 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) )
8 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
9 8 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) )
10 9 biimpar ⊢ ( ( 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
11 biid ⊢ ( ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) ↔ ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) )
12 omex ⊢ ω ∈ V
13 difexg ⊢ ( ω ∈ V → ( ω ∖ { ∅ } ) ∈ V )
14 12 13 ax-mp ⊢ ( ω ∖ { ∅ } ) ∈ V
15 3 14 eqeltri ⊢ 𝐷 ∈ V
16 zfregfr ⊢ E Fr 𝐷
17 11 15 16 bnj157 ⊢ ( ∀ 𝑛 ∈ 𝐷 ( ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) → ∀ 𝑛 ∈ 𝐷 ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) )
18 biid ⊢ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
19 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) )
20 18 2 3 19 11 bnj153 ⊢ ( 𝑛 = 1o → ( ( 𝑛 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) )
21 18 2 3 19 11 bnj601 ⊢ ( 𝑛 ≠ 1o → ( ( 𝑛 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) )
22 20 21 pm2.61ine ⊢ ( ( 𝑛 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) )
23 22 ex ⊢ ( 𝑛 ∈ 𝐷 → ( ∀ 𝑧 ∈ 𝐷 ( 𝑧 E 𝑛 → [ 𝑧 / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ) )
24 17 23 mprg ⊢ ∀ 𝑛 ∈ 𝐷 ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) )
25 r19.21v ⊢ ( ∀ 𝑛 ∈ 𝐷 ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ) )
26 24 25 mpbi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) )
27 10 26 syl ⊢ ( ( 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) )
28 bnj602 ⊢ ( 𝑥 = 𝑋 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
29 28 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) )
30 29 1 bitr4di ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ 𝜑 ) )
31 30 3anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
32 31 eubidv ⊢ ( 𝑥 = 𝑋 → ( ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ↔ ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
33 32 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ↔ ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
34 33 adantr ⊢ ( ( 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝜓 ) ↔ ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
35 27 34 mpbid ⊢ ( ( 𝑥 = 𝑋 ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
36 7 35 bnj593 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
37 36 bnj937 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )