Metamath Proof Explorer

Theorem bnj153

Description: Technical lemma for bnj852 . 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 bnj153.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
bnj153.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj153.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
bnj153.4 ⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
bnj153.5 ⊢ ( 𝜏 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜃 ) )
Assertion bnj153 ( 𝑛 = 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )

Proof

Step Hyp Ref Expression
1 bnj153.1 ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2 bnj153.2 ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 bnj153.3 ⊢ 𝐷 = ( ω ∖ { ∅ } )
4 bnj153.4 ⊢ ( 𝜃 ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
5 bnj153.5 ⊢ ( 𝜏 ↔ ∀ 𝑚 ∈ 𝐷 ( 𝑚 E 𝑛 → [ 𝑚 / 𝑛 ] 𝜃 ) )
6 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
7 biid ⊢ ( [ 1o / 𝑛 ] 𝜑 ↔ [ 1o / 𝑛 ] 𝜑 )
8 1 7 bnj118 ⊢ ( [ 1o / 𝑛 ] 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
9 8 bicomi ⊢ ( ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ [ 1o / 𝑛 ] 𝜑 )
10 bnj105 ⊢ 1o ∈ V
11 2 10 bnj92 ⊢ ( [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
12 11 bicomi ⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 1o / 𝑛 ] 𝜓 )
13 biid ⊢ ( [ 1o / 𝑛 ] 𝜃 ↔ [ 1o / 𝑛 ] 𝜃 )
14 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
15 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃* 𝑓 ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
16 biid ⊢ ( [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
17 biid ⊢ ( [ 1o / 𝑛 ] 𝜓 ↔ [ 1o / 𝑛 ] 𝜓 )
18 6 16 7 17 bnj121 ⊢ ( [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ) )
19 8 anbi2i ⊢ ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ) ↔ ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
20 19 11 anbi12i ⊢ ( ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ) ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
21 df-3an ⊢ ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ) ∧ [ 1o / 𝑛 ] 𝜓 ) )
22 df-3an ⊢ ( ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
23 20 21 22 3bitr4i ⊢ ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
24 23 imbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
25 18 24 bitri ⊢ ( [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
26 25 bicomi ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ↔ [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
27 eqid ⊢ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
28 biid ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
29 biid ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
30 26 sbcbii ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
31 biid ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 )
32 biid ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 )
33 biid ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
34 27 31 32 33 18 bnj124 ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ) )
35 1 7 31 27 bnj125 ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
36 35 anbi2i ⊢ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ↔ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
37 2 17 32 27 bnj126 ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
38 36 37 anbi12i ⊢ ( ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
39 df-3an ⊢ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) )
40 df-3an ⊢ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
41 38 39 40 3bitr4i ⊢ ( ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
42 41 imbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
43 34 42 bitri ⊢ ( [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] [ 1o / 𝑛 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
44 30 43 bitr2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } Fn 1o ∧ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ↔ [ { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ } / 𝑓 ] ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) )
45 biid ⊢ ( ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
46 biid ⊢ ( ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) )
47 biid ⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) )
48 biid ⊢ ( [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 )
49 biid ⊢ ( [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 )
50 46 47 48 49 bnj156 ⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) )
51 48 8 bnj154 ⊢ ( [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ↔ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
52 51 anbi2i ⊢ ( ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ↔ ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
53 17 11 bitri ⊢ ( [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
54 49 53 bnj155 ⊢ ( [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
55 52 54 anbi12i ⊢ ( ( ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
56 df-3an ⊢ ( ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ) ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) )
57 df-3an ⊢ ( ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
58 55 56 57 3bitr4i ⊢ ( ( 𝑔 Fn 1o ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜑 ∧ [ 𝑔 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ) ↔ ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
59 50 58 bitri ⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
60 23 sbcbii ⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ [ 1o / 𝑛 ] 𝜑 ∧ [ 1o / 𝑛 ] 𝜓 ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
61 59 60 bitr3i ⊢ ( ( 𝑔 Fn 1o ∧ ( 𝑔 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑔 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑔 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
62 biid ⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
63 biid ⊢ ( [ 𝑔 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ [ 𝑔 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
64 1 2 3 4 5 6 9 12 13 14 15 26 27 28 29 44 45 61 62 63 bnj151 ⊢ ( 𝑛 = 1o → ( ( 𝑛 ∈ 𝐷 ∧ 𝜏 ) → 𝜃 ) )