Step |
Hyp |
Ref |
Expression |
1 |
|
fmlasuc |
⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) |
3 |
2
|
eleq2d |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) ) |
4 |
|
elun |
⊢ ( 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) |
5 |
4
|
a1i |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) ) |
6 |
|
eqeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
8 |
|
eqeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ∀𝑔 𝑖 𝑢 ↔ 𝐹 = ∀𝑔 𝑖 𝑢 ) ) |
9 |
8
|
rexbidv |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) |
10 |
7 9
|
orbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) |
11 |
10
|
rexbidv |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) |
12 |
11
|
elabg |
⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) |
14 |
13
|
orbi2d |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) ) |
15 |
3 5 14
|
3bitrd |
⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) ) |