Metamath Proof Explorer

Theorem bnj865

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 bnj865.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
bnj865.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj865.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj865.5 ⊢ ( 𝜒 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) )
bnj865.6 ⊢ ( 𝜃 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
Assertion bnj865 ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 )

Proof

Step Hyp Ref Expression
1 bnj865.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2 bnj865.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj865.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj865.5 ⊢ ( 𝜒 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) )
5 bnj865.6 ⊢ ( 𝜃 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
6 1 2 3 bnj852 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
7 omex ⊢ ω ∈ V
8 difexg ⊢ ( ω ∈ V → ( ω ∖ { ∅ } ) ∈ V )
9 7 8 ax-mp ⊢ ( ω ∖ { ∅ } ) ∈ V
10 3 9 eqeltri ⊢ 𝐷 ∈ V
11 raleq ⊢ ( 𝑧 = 𝐷 → ( ∀ 𝑛 ∈ 𝑧 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
12 raleq ⊢ ( 𝑧 = 𝐷 → ( ∀ 𝑛 ∈ 𝑧 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
13 12 exbidv ⊢ ( 𝑧 = 𝐷 → ( ∃ 𝑤 ∀ 𝑛 ∈ 𝑧 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑤 ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
14 11 13 imbi12d ⊢ ( 𝑧 = 𝐷 → ( ( ∀ 𝑛 ∈ 𝑧 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝑧 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
15 zfrep6 ⊢ ( ∀ 𝑛 ∈ 𝑧 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝑧 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
16 10 14 15 vtocl ⊢ ( ∀ 𝑛 ∈ 𝐷 ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
17 6 16 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
18 19.37v ⊢ ( ∃ 𝑤 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑤 ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
19 17 18 mpbir ⊢ ∃ 𝑤 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
20 df-ral ⊢ ( ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑛 ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
21 20 imbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
22 19.21v ⊢ ( ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
23 21 22 bitr4i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
24 23 exbii ⊢ ( ∃ 𝑤 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
25 impexp ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) )
26 df-3an ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) )
27 26 bicomi ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) )
28 27 imbi1i ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
29 25 28 bitr3i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
30 29 albii ⊢ ( ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) ↔ ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
31 30 exbii ⊢ ( ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐷 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) ↔ ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
32 24 31 bitri ⊢ ( ∃ 𝑤 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝐷 ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
33 19 32 mpbi ⊢ ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
34 4 bicomi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) ↔ 𝜒 )
35 34 imbi1i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
36 35 albii ⊢ ( ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
37 36 exbii ⊢ ( ∃ 𝑤 ∀ 𝑛 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
38 33 37 mpbi ⊢ ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
39 5 rexbii ⊢ ( ∃ 𝑓 ∈ 𝑤 𝜃 ↔ ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
40 39 imbi2i ⊢ ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ↔ ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
41 40 albii ⊢ ( ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ↔ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
42 41 exbii ⊢ ( ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ↔ ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
43 38 42 mpbir ⊢ ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 )