Metamath Proof Explorer

Theorem relexpindlem

Description: Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypotheses relexpindlem.1 ⊢ ( 𝜂 → Rel 𝑅 )
relexpindlem.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
relexpindlem.3 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
relexpindlem.4 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
relexpindlem.5 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
relexpindlem.6 ⊢ ( 𝜂 → 𝜒 )
relexpindlem.7 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
Assertion relexpindlem ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 relexpindlem.1 ⊢ ( 𝜂 → Rel 𝑅 )
2 relexpindlem.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
3 relexpindlem.3 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
4 relexpindlem.4 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
5 relexpindlem.5 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
6 relexpindlem.6 ⊢ ( 𝜂 → 𝜒 )
7 relexpindlem.7 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
8 eleq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ∈ ℕ0 ↔ 0 ∈ ℕ0 ) )
9 8 anbi2d ⊢ ( 𝑘 = 0 → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) )
10 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑅 ↑𝑟 𝑘 ) = ( 𝑅 ↑𝑟 0 ) )
11 10 breqd ⊢ ( 𝑘 = 0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 ↔ 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 ) )
12 11 imbi1d ⊢ ( 𝑘 = 0 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ) )
13 12 albidv ⊢ ( 𝑘 = 0 → ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ) )
14 9 13 imbi12d ⊢ ( 𝑘 = 0 → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ) ) )
15 eleq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 ∈ ℕ0 ↔ 𝑙 ∈ ℕ0 ) )
16 15 anbi2d ⊢ ( 𝑘 = 𝑙 → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) ) )
17 oveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑅 ↑𝑟 𝑘 ) = ( 𝑅 ↑𝑟 𝑙 ) )
18 17 breqd ⊢ ( 𝑘 = 𝑙 → ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 ) )
19 18 imbi1d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) )
20 19 albidv ⊢ ( 𝑘 = 𝑙 → ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) )
21 16 20 imbi12d ⊢ ( 𝑘 = 𝑙 → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ) )
22 eleq1 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝑘 ∈ ℕ0 ↔ ( 𝑙 + 1 ) ∈ ℕ0 ) )
23 22 anbi2d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) ) )
24 oveq2 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝑅 ↑𝑟 𝑘 ) = ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) )
25 24 breqd ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 ↔ 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 ) )
26 25 imbi1d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
27 26 albidv ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
28 23 27 imbi12d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) ) )
29 eleq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ∈ ℕ0 ↔ 𝑛 ∈ ℕ0 ) )
30 29 anbi2d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) ) )
31 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑅 ↑𝑟 𝑘 ) = ( 𝑅 ↑𝑟 𝑛 ) )
32 31 breqd ⊢ ( 𝑘 = 𝑛 → ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 ) )
33 32 imbi1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
34 33 albidv ⊢ ( 𝑘 = 𝑛 → ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
35 30 34 imbi12d ⊢ ( 𝑘 = 𝑛 → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑘 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) )
36 1 anim1ci ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑅 ∈ V ∧ Rel 𝑅 ) )
37 36 adantr ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑅 ∈ V ∧ Rel 𝑅 ) )
38 relexp0 ⊢ ( ( 𝑅 ∈ V ∧ Rel 𝑅 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
39 37 38 syl ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
40 6 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝜒 )
41 simpl ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
42 2 ad2antrl ⊢ ( ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → 𝑆 ∈ 𝑉 )
43 simprl ⊢ ( ( 𝑖 = 𝑆 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑆 ) ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
44 43 40 jccil ⊢ ( ( 𝑖 = 𝑆 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑆 ) ) ) → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
45 44 expcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑆 ) ) → ( 𝑖 = 𝑆 → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
46 45 expcom ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑆 ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑖 = 𝑆 → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) ) )
47 46 expcom ⊢ ( 𝑖 = 𝑆 → ( 𝜑 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑖 = 𝑆 → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) ) ) )
48 47 3imp1 ⊢ ( ( ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ 𝑖 = 𝑆 ) → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
49 48 expcom ⊢ ( 𝑖 = 𝑆 → ( ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
50 simprr ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → 𝑖 = 𝑆 )
51 3 ad2antll ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → ( 𝜑 ↔ 𝜒 ) )
52 51 bicomd ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → ( 𝜒 ↔ 𝜑 ) )
53 anbi1 ⊢ ( ( 𝜒 ↔ 𝜑 ) → ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) ↔ ( 𝜑 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) ) )
54 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → 𝜑 )
55 53 54 biimtrdi ⊢ ( ( 𝜒 ↔ 𝜑 ) → ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → 𝜑 ) )
56 52 55 mpcom ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → 𝜑 )
57 simprl ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
58 50 56 57 3jca ⊢ ( ( 𝜒 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑖 = 𝑆 ) ) → ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
59 58 anassrs ⊢ ( ( ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ 𝑖 = 𝑆 ) → ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
60 59 expcom ⊢ ( 𝑖 = 𝑆 → ( ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
61 49 60 impbid ⊢ ( 𝑖 = 𝑆 → ( ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ↔ ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
62 61 spcegv ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
63 42 62 mpcom ⊢ ( ( 𝜒 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
64 40 41 63 syl2an2r ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) )
65 df-br ⊢ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ↔ ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) )
66 65 birani ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) )
67 vex ⊢ 𝑥 ∈ V
68 67 opelresi ⊢ ( ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) )
69 66 68 sylib ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) )
70 simplr ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → ⟨ 𝑆 , 𝑥 ⟩ ∈ I )
71 df-br ⊢ ( 𝑆 I 𝑥 ↔ ⟨ 𝑆 , 𝑥 ⟩ ∈ I )
72 70 71 sylibr ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → 𝑆 I 𝑥 )
73 67 ideq ⊢ ( 𝑆 I 𝑥 ↔ 𝑆 = 𝑥 )
74 72 73 sylib ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → 𝑆 = 𝑥 )
75 69 74 mpancom ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝑆 = 𝑥 )
76 breq1 ⊢ ( 𝑆 = 𝑥 → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ↔ 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ) )
77 eqeq2 ⊢ ( 𝑆 = 𝑥 → ( 𝑖 = 𝑆 ↔ 𝑖 = 𝑥 ) )
78 77 3anbi1d ⊢ ( 𝑆 = 𝑥 → ( ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ↔ ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
79 78 exbidv ⊢ ( 𝑆 = 𝑥 → ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ↔ ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
80 79 anbi1d ⊢ ( 𝑆 = 𝑥 → ( ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ↔ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) )
81 76 80 anbi12d ⊢ ( 𝑆 = 𝑥 → ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ↔ ( 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) )
82 simprl ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → 𝜑 )
83 4 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → ( 𝜑 ↔ 𝜓 ) )
84 82 83 mpbid ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → 𝜓 )
85 84 expcom ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑥 ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝜓 ) )
86 85 expcom ⊢ ( 𝑖 = 𝑥 → ( 𝜑 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝜓 ) ) )
87 86 3imp ⊢ ( ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → 𝜓 )
88 87 exlimiv ⊢ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → 𝜓 )
89 88 ad2antrl ⊢ ( ( 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 )
90 81 89 biimtrdi ⊢ ( 𝑆 = 𝑥 → ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 ) )
91 75 90 mpcom ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 )
92 91 expcom ⊢ ( ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) )
93 64 92 mpancom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) )
94 breq ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 ↔ 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ) )
95 94 imbi1d ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) ) )
96 93 95 imbitrrid ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ) )
97 39 96 mpcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) )
98 97 alrimiv ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) )
99 breq2 ⊢ ( 𝑖 = 𝑥 → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 ) )
100 99 4 imbi12d ⊢ ( 𝑖 = 𝑥 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) )
101 100 cbvalvw ⊢ ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) )
102 101 bicomi ⊢ ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) )
103 imbi2 ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ) )
104 103 anbi1d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ↔ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) )
105 104 anbi2d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ↔ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) )
106 105 anbi2d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) )
107 1 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → Rel 𝑅 )
108 107 adantr ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → Rel 𝑅 )
109 simprrr ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → 𝑙 ∈ ℕ0 )
110 108 109 relexpsucld ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) )
111 simpl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 )
112 2 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝑆 ∈ 𝑉 )
113 112 ad2antrl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝑆 ∈ 𝑉 )
114 brcog ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ↔ ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) )
115 113 67 114 sylancl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ↔ ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) )
116 111 115 mpbid ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) )
117 simprl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
118 simprrl ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → 𝑙 ∈ ℕ0 )
119 118 ad2antll ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → 𝑙 ∈ ℕ0 )
120 simprl ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) )
121 120 ad2antll ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) )
122 117 119 121 mp2and ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) )
123 simprrl ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
124 simprrr ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝑗 𝑅 𝑥 )
125 124 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → 𝑗 𝑅 𝑥 )
126 125 ad2antll ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝑗 𝑅 𝑥 )
127 breq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ) )
128 127 5 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) )
129 128 cbvalvw ⊢ ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
130 id ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) )
131 imbi2 ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ) )
132 131 anbi1d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ↔ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) )
133 132 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ↔ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) )
134 133 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) )
135 134 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ↔ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) )
136 130 135 anbi12d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) ↔ ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) ) )
137 simprrl ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
138 137 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
139 138 ad2antll ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
140 sp ⊢ ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
141 140 adantr ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
142 139 141 mpd ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 )
143 136 142 biimtrdi ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 ) )
144 129 143 ax-mp ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 )
145 7 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
146 123 126 144 145 syl3c ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜓 )
147 122 146 mpancom ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → 𝜓 )
148 147 expcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
149 148 expcom ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
150 149 expcom ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( ( 𝑙 + 1 ) ∈ ℕ0 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) ) )
151 150 anassrs ⊢ ( ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( ( 𝑙 + 1 ) ∈ ℕ0 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) ) )
152 151 impcom ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
153 152 anassrs ⊢ ( ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
154 153 impcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
155 154 anassrs ⊢ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
156 155 impcom ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝜓 )
157 156 anassrs ⊢ ( ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → 𝜓 )
158 116 157 exlimddv ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝜓 )
159 158 expcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
160 breq ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 ↔ 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ) )
161 160 imbi1d ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
162 159 161 imbitrrid ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
163 110 162 mpcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
164 163 alrimiv ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
165 106 164 biimtrdi ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
166 102 165 ax-mp ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
167 166 anassrs ⊢ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
168 167 expcom ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
169 168 expcom ⊢ ( 𝑙 ∈ ℕ0 → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) ) )
170 14 21 28 35 98 169 nn0ind ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
171 170 anabsi7 ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
172 171 19.21bi ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
173 172 exp31 ⊢ ( 𝜂 → ( 𝑅 ∈ V → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) )
174 reldmrelexp ⊢ Rel dom ↑𝑟
175 174 ovprc1 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑛 ) = ∅ )
176 175 breqd ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 ↔ 𝑆 ∅ 𝑥 ) )
177 br0 ⊢ ¬ 𝑆 ∅ 𝑥
178 177 pm2.21i ⊢ ( 𝑆 ∅ 𝑥 → 𝜓 )
179 176 178 biimtrdi ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
180 179 a1d ⊢ ( ¬ 𝑅 ∈ V → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
181 173 180 pm2.61d1 ⊢ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )