Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) |
2 |
|
simpr |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) |
3 |
|
peano2 |
⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω ) |
4 |
3
|
ancri |
⊢ ( 𝑁 ∈ ω → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) |
6 |
|
sssucid |
⊢ 𝑁 ⊆ suc 𝑁 |
7 |
6
|
a1i |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑁 ⊆ suc 𝑁 ) |
8 |
|
eqid |
⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 ) |
9 |
8
|
satfsschain |
⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) → ( 𝑁 ⊆ suc 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) ) |
10 |
9
|
imp |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω ) ) ∧ 𝑁 ⊆ suc 𝑁 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) |
11 |
2 5 7 10
|
syl21anc |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) |
12 |
|
eqid |
⊢ ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) |
13 |
|
eqid |
⊢ { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } |
14 |
8 12 13
|
satffunlem2lem1 |
⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) |
15 |
14
|
expcom |
⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
16 |
11 15
|
syl |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
17 |
16
|
imp |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) |
18 |
8 12 13
|
satffunlem2lem2 |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) = ∅ ) |
19 |
|
funun |
⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∧ Fun { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ∧ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∩ dom { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) = ∅ ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
20 |
1 17 18 19
|
syl21anc |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
21 |
|
simpl |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 ) |
22 |
|
simpr |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 ) |
23 |
|
simpl |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑁 ∈ ω ) |
24 |
8 12 13
|
satfvsucsuc |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
25 |
21 22 23 24
|
syl2an23an |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) |
26 |
25
|
funeqd |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) ) |
27 |
26
|
adantr |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ↔ Fun ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { 〈 𝑖 , 𝑗 〉 } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∨ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∃ 𝑣 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ∖ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) } ) ) ) |
28 |
20 27
|
mpbird |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ) |
29 |
28
|
ex |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑁 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑁 ) ) ) |