Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑎 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) |
2 |
1
|
releqd |
⊢ ( 𝑎 = ∅ → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ) |
3 |
2
|
imbi2d |
⊢ ( 𝑎 = ∅ → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) |
5 |
4
|
releqd |
⊢ ( 𝑎 = 𝑏 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) ) |
6 |
5
|
imbi2d |
⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) |
8 |
7
|
releqd |
⊢ ( 𝑎 = suc 𝑏 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) |
9 |
8
|
imbi2d |
⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑎 = 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) |
11 |
10
|
releqd |
⊢ ( 𝑎 = 𝑁 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) |
12 |
11
|
imbi2d |
⊢ ( 𝑎 = 𝑁 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) ) |
13 |
|
relopabv |
⊢ Rel { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } |
14 |
|
eqid |
⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 ) |
15 |
14
|
satfv0 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) |
16 |
15
|
releqd |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ Rel { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) ) |
17 |
13 16
|
mpbiri |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) |
18 |
|
pm2.27 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) ) |
19 |
|
simpr |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) |
20 |
|
relopabv |
⊢ Rel { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } |
21 |
|
relun |
⊢ ( Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ↔ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∧ Rel { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) |
22 |
19 20 21
|
sylanblrc |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) |
23 |
14
|
satfvsuc |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) |
24 |
23
|
ad4ant123 |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) |
25 |
24
|
releqd |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) ) |
26 |
22 25
|
mpbird |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) |
27 |
26
|
exp31 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑏 ∈ ω → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) ) |
28 |
27
|
com23 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → ( 𝑏 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) ) |
29 |
18 28
|
syld |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( 𝑏 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) ) |
30 |
29
|
com13 |
⊢ ( 𝑏 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) ) |
31 |
3 6 9 12 17 30
|
finds |
⊢ ( 𝑁 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) |
32 |
31
|
com12 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑁 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) |
33 |
32
|
3impia |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) |