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 simpl ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 )
66 df-br ⊢ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ↔ ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) )
67 65 66 sylib ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) )
68 vex ⊢ 𝑥 ∈ V
69 68 opelresi ⊢ ( ⟨ 𝑆 , 𝑥 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) )
70 67 69 sylib ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) )
71 simplr ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → ⟨ 𝑆 , 𝑥 ⟩ ∈ I )
72 df-br ⊢ ( 𝑆 I 𝑥 ↔ ⟨ 𝑆 , 𝑥 ⟩ ∈ I )
73 71 72 sylibr ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → 𝑆 I 𝑥 )
74 68 ideq ⊢ ( 𝑆 I 𝑥 ↔ 𝑆 = 𝑥 )
75 73 74 sylib ⊢ ( ( ( 𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑆 , 𝑥 ⟩ ∈ I ) ∧ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) → 𝑆 = 𝑥 )
76 70 75 mpancom ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝑆 = 𝑥 )
77 breq1 ⊢ ( 𝑆 = 𝑥 → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ↔ 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ) )
78 eqeq2 ⊢ ( 𝑆 = 𝑥 → ( 𝑖 = 𝑆 ↔ 𝑖 = 𝑥 ) )
79 78 3anbi1d ⊢ ( 𝑆 = 𝑥 → ( ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ↔ ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
80 79 exbidv ⊢ ( 𝑆 = 𝑥 → ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ↔ ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ) )
81 80 anbi1d ⊢ ( 𝑆 = 𝑥 → ( ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ↔ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) )
82 77 81 anbi12d ⊢ ( 𝑆 = 𝑥 → ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ↔ ( 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) ) )
83 simprl ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → 𝜑 )
84 4 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → ( 𝜑 ↔ 𝜓 ) )
85 83 84 mpbid ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝜑 ∧ 𝑖 = 𝑥 ) ) → 𝜓 )
86 85 expcom ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑥 ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝜓 ) )
87 86 expcom ⊢ ( 𝑖 = 𝑥 → ( 𝜑 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝜓 ) ) )
88 87 3imp ⊢ ( ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → 𝜓 )
89 88 exlimiv ⊢ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) → 𝜓 )
90 89 ad2antrl ⊢ ( ( 𝑥 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 )
91 82 90 biimtrdi ⊢ ( 𝑆 = 𝑥 → ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 ) )
92 76 91 mpcom ⊢ ( ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ∧ ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) ) → 𝜓 )
93 92 expcom ⊢ ( ( ∃ 𝑖 ( 𝑖 = 𝑆 ∧ 𝜑 ∧ ( 𝜂 ∧ 𝑅 ∈ V ) ) ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) ) → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) )
94 64 93 mpancom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) )
95 breq ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 ↔ 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 ) )
96 95 imbi1d ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( I ↾ ∪ ∪ 𝑅 ) 𝑥 → 𝜓 ) ) )
97 94 96 imbitrrid ⊢ ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) ) )
98 39 97 mpcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) )
99 98 alrimiv ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 0 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 0 ) 𝑥 → 𝜓 ) )
100 breq2 ⊢ ( 𝑖 = 𝑥 → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 ) )
101 100 4 imbi12d ⊢ ( 𝑖 = 𝑥 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) )
102 101 cbvalvw ⊢ ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) )
103 102 bicomi ⊢ ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) )
104 imbi2 ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ) )
105 104 anbi1d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ↔ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) )
106 105 anbi2d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ↔ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) )
107 106 anbi2d ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) )
108 1 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → Rel 𝑅 )
109 108 adantr ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → Rel 𝑅 )
110 simprrr ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → 𝑙 ∈ ℕ0 )
111 109 110 relexpsucld ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) )
112 simpl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 )
113 2 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → 𝑆 ∈ 𝑉 )
114 113 ad2antrl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝑆 ∈ 𝑉 )
115 brcog ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ↔ ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) )
116 114 68 115 sylancl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ↔ ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) )
117 112 116 mpbid ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → ∃ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) )
118 simprl ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
119 simprrl ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → 𝑙 ∈ ℕ0 )
120 119 ad2antll ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → 𝑙 ∈ ℕ0 )
121 simprl ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) )
122 121 ad2antll ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) )
123 118 120 122 mp2and ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) )
124 simprrl ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → ( 𝜂 ∧ 𝑅 ∈ V ) )
125 simprrr ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝑗 𝑅 𝑥 )
126 125 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → 𝑗 𝑅 𝑥 )
127 126 ad2antll ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝑗 𝑅 𝑥 )
128 breq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ) )
129 128 5 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) )
130 129 cbvalvw ⊢ ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
131 id ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) )
132 imbi2 ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ↔ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ) )
133 132 anbi1d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ↔ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) )
134 133 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ↔ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) )
135 134 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ↔ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) )
136 135 anbi2d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ↔ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) )
137 131 136 anbi12d ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) ↔ ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) ) )
138 simprrl ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
139 138 ad2antll ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
140 139 ad2antll ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 )
141 sp ⊢ ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
142 141 adantr ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) )
143 140 142 mpd ⊢ ( ( ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 )
144 137 143 biimtrdi ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ↔ ∀ 𝑗 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 → 𝜃 ) ) → ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 ) )
145 130 144 ax-mp ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜃 )
146 7 adantr ⊢ ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
147 124 127 145 146 syl3c ⊢ ( ( ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ∧ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) ) → 𝜓 )
148 123 147 mpancom ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) ) → 𝜓 )
149 148 expcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
150 149 expcom ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
151 150 expcom ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ ( 𝑙 ∈ ℕ0 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( ( 𝑙 + 1 ) ∈ ℕ0 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) ) )
152 151 anassrs ⊢ ( ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( ( 𝑙 + 1 ) ∈ ℕ0 → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) ) )
153 152 impcom ⊢ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
154 153 anassrs ⊢ ( ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( ( 𝜂 ∧ 𝑅 ∈ V ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
155 154 impcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
156 155 anassrs ⊢ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
157 156 impcom ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) ) → 𝜓 )
158 157 anassrs ⊢ ( ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑗 ∧ 𝑗 𝑅 𝑥 ) ) → 𝜓 )
159 117 158 exlimddv ⊢ ( ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ∧ ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) ) → 𝜓 )
160 159 expcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) )
161 breq ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 ↔ 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 ) )
162 161 imbi1d ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) 𝑥 → 𝜓 ) ) )
163 160 162 imbitrrid ⊢ ( ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑙 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
164 111 163 mpcom ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
165 164 alrimiv ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
166 107 165 biimtrdi ⊢ ( ( ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ↔ ∀ 𝑖 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑖 → 𝜑 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
167 103 166 ax-mp ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑙 + 1 ) ∈ ℕ0 ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
168 167 anassrs ⊢ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) ∧ ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) )
169 168 expcom ⊢ ( ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) )
170 169 expcom ⊢ ( 𝑙 ∈ ℕ0 → ( ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑙 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑙 ) 𝑥 → 𝜓 ) ) → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ ( 𝑙 + 1 ) ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 ( 𝑙 + 1 ) ) 𝑥 → 𝜓 ) ) ) )
171 14 21 28 35 99 170 nn0ind ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
172 171 anabsi7 ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑥 ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
173 172 19.21bi ⊢ ( ( ( 𝜂 ∧ 𝑅 ∈ V ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
174 173 exp31 ⊢ ( 𝜂 → ( 𝑅 ∈ V → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) )
175 reldmrelexp ⊢ Rel dom ↑𝑟
176 175 ovprc1 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑛 ) = ∅ )
177 176 breqd ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 ↔ 𝑆 ∅ 𝑥 ) )
178 br0 ⊢ ¬ 𝑆 ∅ 𝑥
179 178 pm2.21i ⊢ ( 𝑆 ∅ 𝑥 → 𝜓 )
180 177 179 biimtrdi ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) )
181 180 a1d ⊢ ( ¬ 𝑅 ∈ V → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
182 174 181 pm2.61d1 ⊢ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )