| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oveq1 |
⊢ ( 𝑝 = 𝑟 → ( 𝑝 ·no 𝑞 ) = ( 𝑟 ·no 𝑞 ) ) |
| 2 |
1
|
eleq1d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 ·no 𝑞 ) ∈ On ↔ ( 𝑟 ·no 𝑞 ) ∈ On ) ) |
| 3 |
|
oveq1 |
⊢ ( 𝑝 = 𝑟 → ( 𝑝 ·no 𝑏 ) = ( 𝑟 ·no 𝑏 ) ) |
| 4 |
3
|
oveq2d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) = ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ) |
| 5 |
4
|
eleq1d |
⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 6 |
5
|
ralbidv |
⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 7 |
6
|
raleqbi1dv |
⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 8 |
7
|
rabbidv |
⊢ ( 𝑝 = 𝑟 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 9 |
8
|
inteqd |
⊢ ( 𝑝 = 𝑟 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 10 |
1 9
|
eqeq12d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 11 |
2 10
|
anbi12d |
⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑝 ·no 𝑞 ) ∈ On ∧ ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ↔ ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 12 |
|
oveq2 |
⊢ ( 𝑞 = 𝑠 → ( 𝑟 ·no 𝑞 ) = ( 𝑟 ·no 𝑠 ) ) |
| 13 |
12
|
eleq1d |
⊢ ( 𝑞 = 𝑠 → ( ( 𝑟 ·no 𝑞 ) ∈ On ↔ ( 𝑟 ·no 𝑠 ) ∈ On ) ) |
| 14 |
|
oveq2 |
⊢ ( 𝑞 = 𝑠 → ( 𝑎 ·no 𝑞 ) = ( 𝑎 ·no 𝑠 ) ) |
| 15 |
14
|
oveq1d |
⊢ ( 𝑞 = 𝑠 → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) = ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ) |
| 16 |
15
|
eleq1d |
⊢ ( 𝑞 = 𝑠 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 17 |
16
|
raleqbi1dv |
⊢ ( 𝑞 = 𝑠 → ( ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 18 |
17
|
ralbidv |
⊢ ( 𝑞 = 𝑠 → ( ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 19 |
18
|
rabbidv |
⊢ ( 𝑞 = 𝑠 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 20 |
19
|
inteqd |
⊢ ( 𝑞 = 𝑠 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 21 |
12 20
|
eqeq12d |
⊢ ( 𝑞 = 𝑠 → ( ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 22 |
13 21
|
anbi12d |
⊢ ( 𝑞 = 𝑠 → ( ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ↔ ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 23 |
|
oveq1 |
⊢ ( 𝑝 = 𝑟 → ( 𝑝 ·no 𝑠 ) = ( 𝑟 ·no 𝑠 ) ) |
| 24 |
23
|
eleq1d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 ·no 𝑠 ) ∈ On ↔ ( 𝑟 ·no 𝑠 ) ∈ On ) ) |
| 25 |
3
|
oveq2d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) = ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ) |
| 26 |
25
|
eleq1d |
⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 27 |
26
|
ralbidv |
⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 28 |
27
|
raleqbi1dv |
⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 29 |
28
|
rabbidv |
⊢ ( 𝑝 = 𝑟 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 30 |
29
|
inteqd |
⊢ ( 𝑝 = 𝑟 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 31 |
23 30
|
eqeq12d |
⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 32 |
24 31
|
anbi12d |
⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑝 ·no 𝑠 ) ∈ On ∧ ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ↔ ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 33 |
|
oveq1 |
⊢ ( 𝑝 = 𝐴 → ( 𝑝 ·no 𝑞 ) = ( 𝐴 ·no 𝑞 ) ) |
| 34 |
33
|
eleq1d |
⊢ ( 𝑝 = 𝐴 → ( ( 𝑝 ·no 𝑞 ) ∈ On ↔ ( 𝐴 ·no 𝑞 ) ∈ On ) ) |
| 35 |
|
oveq1 |
⊢ ( 𝑝 = 𝐴 → ( 𝑝 ·no 𝑏 ) = ( 𝐴 ·no 𝑏 ) ) |
| 36 |
35
|
oveq2d |
⊢ ( 𝑝 = 𝐴 → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) = ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ) |
| 37 |
36
|
eleq1d |
⊢ ( 𝑝 = 𝐴 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 38 |
37
|
ralbidv |
⊢ ( 𝑝 = 𝐴 → ( ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 39 |
38
|
raleqbi1dv |
⊢ ( 𝑝 = 𝐴 → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 40 |
39
|
rabbidv |
⊢ ( 𝑝 = 𝐴 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 41 |
40
|
inteqd |
⊢ ( 𝑝 = 𝐴 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 42 |
33 41
|
eqeq12d |
⊢ ( 𝑝 = 𝐴 → ( ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ( 𝐴 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 43 |
34 42
|
anbi12d |
⊢ ( 𝑝 = 𝐴 → ( ( ( 𝑝 ·no 𝑞 ) ∈ On ∧ ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ↔ ( ( 𝐴 ·no 𝑞 ) ∈ On ∧ ( 𝐴 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 44 |
|
oveq2 |
⊢ ( 𝑞 = 𝐵 → ( 𝐴 ·no 𝑞 ) = ( 𝐴 ·no 𝐵 ) ) |
| 45 |
44
|
eleq1d |
⊢ ( 𝑞 = 𝐵 → ( ( 𝐴 ·no 𝑞 ) ∈ On ↔ ( 𝐴 ·no 𝐵 ) ∈ On ) ) |
| 46 |
|
oveq2 |
⊢ ( 𝑞 = 𝐵 → ( 𝑎 ·no 𝑞 ) = ( 𝑎 ·no 𝐵 ) ) |
| 47 |
46
|
oveq1d |
⊢ ( 𝑞 = 𝐵 → ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) = ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ) |
| 48 |
47
|
eleq1d |
⊢ ( 𝑞 = 𝐵 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 49 |
48
|
raleqbi1dv |
⊢ ( 𝑞 = 𝐵 → ( ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 50 |
49
|
ralbidv |
⊢ ( 𝑞 = 𝐵 → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 51 |
50
|
rabbidv |
⊢ ( 𝑞 = 𝐵 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 52 |
51
|
inteqd |
⊢ ( 𝑞 = 𝐵 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 53 |
44 52
|
eqeq12d |
⊢ ( 𝑞 = 𝐵 → ( ( 𝐴 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 54 |
45 53
|
anbi12d |
⊢ ( 𝑞 = 𝐵 → ( ( ( 𝐴 ·no 𝑞 ) ∈ On ∧ ( 𝐴 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ↔ ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 55 |
|
simpl |
⊢ ( ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ( 𝑟 ·no 𝑠 ) ∈ On ) |
| 56 |
55
|
2ralimi |
⊢ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ) |
| 57 |
|
simpl |
⊢ ( ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 58 |
57
|
ralimi |
⊢ ( ∀ 𝑟 ∈ 𝑝 ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 59 |
|
simpl |
⊢ ( ( ( 𝑝 ·no 𝑠 ) ∈ On ∧ ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 60 |
59
|
ralimi |
⊢ ( ∀ 𝑠 ∈ 𝑞 ( ( 𝑝 ·no 𝑠 ) ∈ On ∧ ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 61 |
56 58 60
|
3anim123i |
⊢ ( ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ∧ ∀ 𝑟 ∈ 𝑝 ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ∧ ∀ 𝑠 ∈ 𝑞 ( ( 𝑝 ·no 𝑠 ) ∈ On ∧ ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) → ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) |
| 62 |
|
df-nmul |
⊢ ·no = frecs ( { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( On × On ) ∧ 𝑢 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑡 ) E ( 1st ‘ 𝑢 ) ∨ ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑢 ) ) ∧ ( ( 2nd ‘ 𝑡 ) E ( 2nd ‘ 𝑢 ) ∨ ( 2nd ‘ 𝑡 ) = ( 2nd ‘ 𝑢 ) ) ∧ 𝑡 ≠ 𝑢 ) ) } , ( On × On ) , ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) ) |
| 63 |
62
|
on2recsov |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( 𝑝 ·no 𝑞 ) = ( ⟨ 𝑝 , 𝑞 ⟩ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ) ) |
| 64 |
63
|
adantr |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( 𝑝 ·no 𝑞 ) = ( ⟨ 𝑝 , 𝑞 ⟩ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ) ) |
| 65 |
|
opex |
⊢ ⟨ 𝑝 , 𝑞 ⟩ ∈ V |
| 66 |
|
nmulfn |
⊢ ·no Fn ( On × On ) |
| 67 |
|
fnfun |
⊢ ( ·no Fn ( On × On ) → Fun ·no ) |
| 68 |
66 67
|
ax-mp |
⊢ Fun ·no |
| 69 |
|
vex |
⊢ 𝑝 ∈ V |
| 70 |
69
|
sucex |
⊢ suc 𝑝 ∈ V |
| 71 |
|
vex |
⊢ 𝑞 ∈ V |
| 72 |
71
|
sucex |
⊢ suc 𝑞 ∈ V |
| 73 |
70 72
|
xpex |
⊢ ( suc 𝑝 × suc 𝑞 ) ∈ V |
| 74 |
73
|
difexi |
⊢ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ∈ V |
| 75 |
|
resfunexg |
⊢ ( ( Fun ·no ∧ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ∈ V ) → ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ∈ V ) |
| 76 |
68 74 75
|
mp2an |
⊢ ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ∈ V |
| 77 |
|
elelsuc |
⊢ ( 𝑎 ∈ 𝑝 → 𝑎 ∈ suc 𝑝 ) |
| 78 |
77
|
adantr |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → 𝑎 ∈ suc 𝑝 ) |
| 79 |
78
|
adantl |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑎 ∈ suc 𝑝 ) |
| 80 |
71
|
sucid |
⊢ 𝑞 ∈ suc 𝑞 |
| 81 |
80
|
a1i |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑞 ∈ suc 𝑞 ) |
| 82 |
79 81
|
opelxpd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑎 , 𝑞 ⟩ ∈ ( suc 𝑝 × suc 𝑞 ) ) |
| 83 |
|
eloni |
⊢ ( 𝑝 ∈ On → Ord 𝑝 ) |
| 84 |
|
ordirr |
⊢ ( Ord 𝑝 → ¬ 𝑝 ∈ 𝑝 ) |
| 85 |
|
elequ1 |
⊢ ( 𝑎 = 𝑝 → ( 𝑎 ∈ 𝑝 ↔ 𝑝 ∈ 𝑝 ) ) |
| 86 |
85
|
notbid |
⊢ ( 𝑎 = 𝑝 → ( ¬ 𝑎 ∈ 𝑝 ↔ ¬ 𝑝 ∈ 𝑝 ) ) |
| 87 |
86
|
biimprcd |
⊢ ( ¬ 𝑝 ∈ 𝑝 → ( 𝑎 = 𝑝 → ¬ 𝑎 ∈ 𝑝 ) ) |
| 88 |
87
|
con2d |
⊢ ( ¬ 𝑝 ∈ 𝑝 → ( 𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝 ) ) |
| 89 |
83 84 88
|
3syl |
⊢ ( 𝑝 ∈ On → ( 𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝 ) ) |
| 90 |
89
|
imp |
⊢ ( ( 𝑝 ∈ On ∧ 𝑎 ∈ 𝑝 ) → ¬ 𝑎 = 𝑝 ) |
| 91 |
90
|
ad2ant2r |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ 𝑎 = 𝑝 ) |
| 92 |
91
|
intnanrd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ( 𝑎 = 𝑝 ∧ 𝑞 = 𝑞 ) ) |
| 93 |
|
opex |
⊢ ⟨ 𝑎 , 𝑞 ⟩ ∈ V |
| 94 |
93
|
elsn |
⊢ ( ⟨ 𝑎 , 𝑞 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ↔ ⟨ 𝑎 , 𝑞 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ) |
| 95 |
|
vex |
⊢ 𝑎 ∈ V |
| 96 |
95 71
|
opth |
⊢ ( ⟨ 𝑎 , 𝑞 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ↔ ( 𝑎 = 𝑝 ∧ 𝑞 = 𝑞 ) ) |
| 97 |
94 96
|
bitr2i |
⊢ ( ( 𝑎 = 𝑝 ∧ 𝑞 = 𝑞 ) ↔ ⟨ 𝑎 , 𝑞 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 98 |
92 97
|
sylnib |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ⟨ 𝑎 , 𝑞 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 99 |
82 98
|
eldifd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑎 , 𝑞 ⟩ ∈ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) |
| 100 |
99
|
fvresd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑎 , 𝑞 ⟩ ) = ( ·no ‘ ⟨ 𝑎 , 𝑞 ⟩ ) ) |
| 101 |
|
df-ov |
⊢ ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) = ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑎 , 𝑞 ⟩ ) |
| 102 |
|
df-ov |
⊢ ( 𝑎 ·no 𝑞 ) = ( ·no ‘ ⟨ 𝑎 , 𝑞 ⟩ ) |
| 103 |
100 101 102
|
3eqtr4g |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) = ( 𝑎 ·no 𝑞 ) ) |
| 104 |
69
|
sucid |
⊢ 𝑝 ∈ suc 𝑝 |
| 105 |
104
|
a1i |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑝 ∈ suc 𝑝 ) |
| 106 |
|
elelsuc |
⊢ ( 𝑏 ∈ 𝑞 → 𝑏 ∈ suc 𝑞 ) |
| 107 |
106
|
adantl |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → 𝑏 ∈ suc 𝑞 ) |
| 108 |
107
|
adantl |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑏 ∈ suc 𝑞 ) |
| 109 |
105 108
|
opelxpd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑝 , 𝑏 ⟩ ∈ ( suc 𝑝 × suc 𝑞 ) ) |
| 110 |
|
eloni |
⊢ ( 𝑞 ∈ On → Ord 𝑞 ) |
| 111 |
|
ordirr |
⊢ ( Ord 𝑞 → ¬ 𝑞 ∈ 𝑞 ) |
| 112 |
|
elequ1 |
⊢ ( 𝑏 = 𝑞 → ( 𝑏 ∈ 𝑞 ↔ 𝑞 ∈ 𝑞 ) ) |
| 113 |
112
|
notbid |
⊢ ( 𝑏 = 𝑞 → ( ¬ 𝑏 ∈ 𝑞 ↔ ¬ 𝑞 ∈ 𝑞 ) ) |
| 114 |
113
|
biimprcd |
⊢ ( ¬ 𝑞 ∈ 𝑞 → ( 𝑏 = 𝑞 → ¬ 𝑏 ∈ 𝑞 ) ) |
| 115 |
114
|
con2d |
⊢ ( ¬ 𝑞 ∈ 𝑞 → ( 𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞 ) ) |
| 116 |
110 111 115
|
3syl |
⊢ ( 𝑞 ∈ On → ( 𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞 ) ) |
| 117 |
116
|
imp |
⊢ ( ( 𝑞 ∈ On ∧ 𝑏 ∈ 𝑞 ) → ¬ 𝑏 = 𝑞 ) |
| 118 |
117
|
ad2ant2l |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ 𝑏 = 𝑞 ) |
| 119 |
118
|
intnand |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ( 𝑝 = 𝑝 ∧ 𝑏 = 𝑞 ) ) |
| 120 |
|
opex |
⊢ ⟨ 𝑝 , 𝑏 ⟩ ∈ V |
| 121 |
120
|
elsn |
⊢ ( ⟨ 𝑝 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ↔ ⟨ 𝑝 , 𝑏 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ) |
| 122 |
|
vex |
⊢ 𝑏 ∈ V |
| 123 |
69 122
|
opth |
⊢ ( ⟨ 𝑝 , 𝑏 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ↔ ( 𝑝 = 𝑝 ∧ 𝑏 = 𝑞 ) ) |
| 124 |
121 123
|
bitr2i |
⊢ ( ( 𝑝 = 𝑝 ∧ 𝑏 = 𝑞 ) ↔ ⟨ 𝑝 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 125 |
119 124
|
sylnib |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ⟨ 𝑝 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 126 |
109 125
|
eldifd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑝 , 𝑏 ⟩ ∈ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) |
| 127 |
126
|
fvresd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑝 , 𝑏 ⟩ ) = ( ·no ‘ ⟨ 𝑝 , 𝑏 ⟩ ) ) |
| 128 |
|
df-ov |
⊢ ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) = ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑝 , 𝑏 ⟩ ) |
| 129 |
|
df-ov |
⊢ ( 𝑝 ·no 𝑏 ) = ( ·no ‘ ⟨ 𝑝 , 𝑏 ⟩ ) |
| 130 |
127 128 129
|
3eqtr4g |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) = ( 𝑝 ·no 𝑏 ) ) |
| 131 |
103 130
|
oveq12d |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) = ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ) |
| 132 |
|
sssucid |
⊢ 𝑝 ⊆ suc 𝑝 |
| 133 |
|
sssucid |
⊢ 𝑞 ⊆ suc 𝑞 |
| 134 |
|
xpss12 |
⊢ ( ( 𝑝 ⊆ suc 𝑝 ∧ 𝑞 ⊆ suc 𝑞 ) → ( 𝑝 × 𝑞 ) ⊆ ( suc 𝑝 × suc 𝑞 ) ) |
| 135 |
132 133 134
|
mp2an |
⊢ ( 𝑝 × 𝑞 ) ⊆ ( suc 𝑝 × suc 𝑞 ) |
| 136 |
|
opelxpi |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑝 × 𝑞 ) ) |
| 137 |
135 136
|
sselid |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( suc 𝑝 × suc 𝑞 ) ) |
| 138 |
137
|
adantl |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( suc 𝑝 × suc 𝑞 ) ) |
| 139 |
118
|
intnand |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ( 𝑎 = 𝑝 ∧ 𝑏 = 𝑞 ) ) |
| 140 |
|
opex |
⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V |
| 141 |
140
|
elsn |
⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ) |
| 142 |
95 122
|
opth |
⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑝 , 𝑞 ⟩ ↔ ( 𝑎 = 𝑝 ∧ 𝑏 = 𝑞 ) ) |
| 143 |
141 142
|
bitr2i |
⊢ ( ( 𝑎 = 𝑝 ∧ 𝑏 = 𝑞 ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 144 |
139 143
|
sylnib |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑝 , 𝑞 ⟩ } ) |
| 145 |
138 144
|
eldifd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) |
| 146 |
145
|
fvresd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ( ·no ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) |
| 147 |
|
df-ov |
⊢ ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) = ( ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) |
| 148 |
|
df-ov |
⊢ ( 𝑎 ·no 𝑏 ) = ( ·no ‘ ⟨ 𝑎 , 𝑏 ⟩ ) |
| 149 |
146 147 148
|
3eqtr4g |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) = ( 𝑎 ·no 𝑏 ) ) |
| 150 |
149
|
oveq2d |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) = ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) |
| 151 |
131 150
|
eleq12d |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 152 |
151
|
2ralbidva |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 153 |
152
|
rabbidv |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 154 |
153
|
inteqd |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 155 |
154
|
adantr |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 156 |
|
oveq1 |
⊢ ( 𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) = ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) |
| 157 |
156
|
eleq2d |
⊢ ( 𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 158 |
157
|
2ralbidv |
⊢ ( 𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) ) |
| 159 |
|
ovex |
⊢ ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ V |
| 160 |
71 159
|
iunex |
⊢ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ V |
| 161 |
160
|
dfiun2 |
⊢ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) = ∪ { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } |
| 162 |
159
|
dfiun2 |
⊢ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) = ∪ { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } |
| 163 |
|
oveq1 |
⊢ ( 𝑟 = 𝑐 → ( 𝑟 ·no 𝑞 ) = ( 𝑐 ·no 𝑞 ) ) |
| 164 |
163
|
eleq1d |
⊢ ( 𝑟 = 𝑐 → ( ( 𝑟 ·no 𝑞 ) ∈ On ↔ ( 𝑐 ·no 𝑞 ) ∈ On ) ) |
| 165 |
|
simplr2 |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 166 |
165
|
adantr |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 167 |
|
simplr |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → 𝑐 ∈ 𝑝 ) |
| 168 |
164 166 167
|
rspcdva |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑐 ·no 𝑞 ) ∈ On ) |
| 169 |
|
oveq2 |
⊢ ( 𝑠 = 𝑑 → ( 𝑝 ·no 𝑠 ) = ( 𝑝 ·no 𝑑 ) ) |
| 170 |
169
|
eleq1d |
⊢ ( 𝑠 = 𝑑 → ( ( 𝑝 ·no 𝑠 ) ∈ On ↔ ( 𝑝 ·no 𝑑 ) ∈ On ) ) |
| 171 |
|
simplr3 |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 172 |
171
|
adantr |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 173 |
|
simpr |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → 𝑑 ∈ 𝑞 ) |
| 174 |
170 172 173
|
rspcdva |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑝 ·no 𝑑 ) ∈ On ) |
| 175 |
168 174
|
naddcld |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 176 |
|
eleq1 |
⊢ ( 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( 𝑥 ∈ On ↔ ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) ) |
| 177 |
175 176
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 178 |
177
|
rexlimdva |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ( ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 179 |
178
|
abssdv |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On ) |
| 180 |
71
|
abrexex |
⊢ { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ V |
| 181 |
180
|
ssonunii |
⊢ ( { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On → ∪ { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 182 |
179 181
|
syl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ∪ { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 183 |
162 182
|
eqeltrid |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 184 |
|
eleq1 |
⊢ ( 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( 𝑥 ∈ On ↔ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) ) |
| 185 |
183 184
|
syl5ibrcom |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ 𝑐 ∈ 𝑝 ) → ( 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 186 |
185
|
rexlimdva |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 187 |
186
|
abssdv |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On ) |
| 188 |
69
|
abrexex |
⊢ { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ V |
| 189 |
188
|
ssonunii |
⊢ ( { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On → ∪ { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 190 |
187 189
|
syl |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∪ { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 191 |
161 190
|
eqeltrid |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 192 |
|
onsuc |
⊢ ( ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 193 |
191 192
|
syl |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 194 |
|
simplr2 |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 195 |
164
|
rspccva |
⊢ ( ( ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ 𝑐 ∈ 𝑝 ) → ( 𝑐 ·no 𝑞 ) ∈ On ) |
| 196 |
194 195
|
sylan |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ( 𝑐 ·no 𝑞 ) ∈ On ) |
| 197 |
196
|
adantr |
⊢ ( ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑐 ·no 𝑞 ) ∈ On ) |
| 198 |
|
simplr3 |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 199 |
198
|
adantr |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 200 |
170
|
rspccva |
⊢ ( ( ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ∧ 𝑑 ∈ 𝑞 ) → ( 𝑝 ·no 𝑑 ) ∈ On ) |
| 201 |
199 200
|
sylan |
⊢ ( ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑝 ·no 𝑑 ) ∈ On ) |
| 202 |
197 201
|
naddcld |
⊢ ( ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 203 |
202 176
|
syl5ibrcom |
⊢ ( ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) ∧ 𝑑 ∈ 𝑞 ) → ( 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 204 |
203
|
rexlimdva |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ( ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 205 |
204
|
abssdv |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On ) |
| 206 |
205 181
|
syl |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ∪ { 𝑥 ∣ ∃ 𝑑 ∈ 𝑞 𝑥 = ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 207 |
162 206
|
eqeltrid |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 208 |
207 184
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) ∧ 𝑐 ∈ 𝑝 ) → ( 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 209 |
208
|
rexlimdva |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → 𝑥 ∈ On ) ) |
| 210 |
209
|
abssdv |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ⊆ On ) |
| 211 |
210 189
|
syl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∪ { 𝑥 ∣ ∃ 𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) } ∈ On ) |
| 212 |
161 211
|
eqeltrid |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 213 |
212 192
|
syl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) |
| 214 |
|
oveq1 |
⊢ ( 𝑟 = 𝑎 → ( 𝑟 ·no 𝑠 ) = ( 𝑎 ·no 𝑠 ) ) |
| 215 |
214
|
eleq1d |
⊢ ( 𝑟 = 𝑎 → ( ( 𝑟 ·no 𝑠 ) ∈ On ↔ ( 𝑎 ·no 𝑠 ) ∈ On ) ) |
| 216 |
|
oveq2 |
⊢ ( 𝑠 = 𝑏 → ( 𝑎 ·no 𝑠 ) = ( 𝑎 ·no 𝑏 ) ) |
| 217 |
216
|
eleq1d |
⊢ ( 𝑠 = 𝑏 → ( ( 𝑎 ·no 𝑠 ) ∈ On ↔ ( 𝑎 ·no 𝑏 ) ∈ On ) ) |
| 218 |
|
simplr1 |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ) |
| 219 |
|
simprl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑎 ∈ 𝑝 ) |
| 220 |
|
simprr |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → 𝑏 ∈ 𝑞 ) |
| 221 |
215 217 218 219 220
|
rspc2dv |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑎 ·no 𝑏 ) ∈ On ) |
| 222 |
|
naddword1 |
⊢ ( ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ∧ ( 𝑎 ·no 𝑏 ) ∈ On ) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ⊆ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) |
| 223 |
213 221 222
|
syl2anc |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ⊆ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) |
| 224 |
|
oveq1 |
⊢ ( 𝑐 = 𝑎 → ( 𝑐 ·no 𝑞 ) = ( 𝑎 ·no 𝑞 ) ) |
| 225 |
224
|
oveq1d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) = ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 226 |
225
|
iuneq2d |
⊢ ( 𝑐 = 𝑎 → ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) = ∪ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 227 |
226
|
sseq2d |
⊢ ( 𝑐 = 𝑎 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) ) |
| 228 |
|
oveq2 |
⊢ ( 𝑑 = 𝑏 → ( 𝑝 ·no 𝑑 ) = ( 𝑝 ·no 𝑏 ) ) |
| 229 |
228
|
oveq2d |
⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) = ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ) |
| 230 |
229
|
sseq2d |
⊢ ( 𝑑 = 𝑏 → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ) ) |
| 231 |
|
ssidd |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ) |
| 232 |
230 220 231
|
rspcedvdw |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∃ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 233 |
|
ssiun |
⊢ ( ∃ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 234 |
232 233
|
syl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 235 |
227 219 234
|
rspcedvdw |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ∃ 𝑐 ∈ 𝑝 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 236 |
|
ssiun |
⊢ ( ∃ 𝑐 ∈ 𝑝 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 237 |
235 236
|
syl |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 238 |
|
simpr2 |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ) |
| 239 |
|
simpl |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → 𝑎 ∈ 𝑝 ) |
| 240 |
|
oveq1 |
⊢ ( 𝑟 = 𝑎 → ( 𝑟 ·no 𝑞 ) = ( 𝑎 ·no 𝑞 ) ) |
| 241 |
240
|
eleq1d |
⊢ ( 𝑟 = 𝑎 → ( ( 𝑟 ·no 𝑞 ) ∈ On ↔ ( 𝑎 ·no 𝑞 ) ∈ On ) ) |
| 242 |
241
|
rspccva |
⊢ ( ( ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ 𝑎 ∈ 𝑝 ) → ( 𝑎 ·no 𝑞 ) ∈ On ) |
| 243 |
238 239 242
|
syl2an |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑎 ·no 𝑞 ) ∈ On ) |
| 244 |
|
simpr3 |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) |
| 245 |
|
simpr |
⊢ ( ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) → 𝑏 ∈ 𝑞 ) |
| 246 |
|
oveq2 |
⊢ ( 𝑠 = 𝑏 → ( 𝑝 ·no 𝑠 ) = ( 𝑝 ·no 𝑏 ) ) |
| 247 |
246
|
eleq1d |
⊢ ( 𝑠 = 𝑏 → ( ( 𝑝 ·no 𝑠 ) ∈ On ↔ ( 𝑝 ·no 𝑏 ) ∈ On ) ) |
| 248 |
247
|
rspccva |
⊢ ( ( ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ∧ 𝑏 ∈ 𝑞 ) → ( 𝑝 ·no 𝑏 ) ∈ On ) |
| 249 |
244 245 248
|
syl2an |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( 𝑝 ·no 𝑏 ) ∈ On ) |
| 250 |
243 249
|
naddcld |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ On ) |
| 251 |
|
onsssuc |
⊢ ( ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ On ∧ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ∈ On ) → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) ) |
| 252 |
250 212 251
|
syl2anc |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ↔ ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) ) |
| 253 |
237 252
|
mpbid |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) ) |
| 254 |
223 253
|
sseldd |
⊢ ( ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) ∧ ( 𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞 ) ) → ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) |
| 255 |
254
|
ralrimivva |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ( ( 𝑐 ·no 𝑞 ) +no ( 𝑝 ·no 𝑑 ) ) +no ( 𝑎 ·no 𝑏 ) ) ) |
| 256 |
158 193 255
|
rspcedvdw |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∃ 𝑥 ∈ On ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ) |
| 257 |
|
onintrab2 |
⊢ ( ∃ 𝑥 ∈ On ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ∈ On ) |
| 258 |
256 257
|
sylib |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ∈ On ) |
| 259 |
155 258
|
eqeltrd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ∈ On ) |
| 260 |
69 71
|
op1std |
⊢ ( 𝑣 = ⟨ 𝑝 , 𝑞 ⟩ → ( 1st ‘ 𝑣 ) = 𝑝 ) |
| 261 |
69 71
|
op2ndd |
⊢ ( 𝑣 = ⟨ 𝑝 , 𝑞 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑞 ) |
| 262 |
261
|
csbeq1d |
⊢ ( 𝑣 = ⟨ 𝑝 , 𝑞 ⟩ → ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 263 |
260 262
|
csbeq12dv |
⊢ ( 𝑣 = ⟨ 𝑝 , 𝑞 ⟩ → ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ⦋ 𝑝 / 𝑐 ⦌ ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 264 |
|
oveq1 |
⊢ ( 𝑐 = 𝑝 → ( 𝑐 𝑤 𝑏 ) = ( 𝑝 𝑤 𝑏 ) ) |
| 265 |
264
|
oveq2d |
⊢ ( 𝑐 = 𝑝 → ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) = ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ) |
| 266 |
265
|
eleq1d |
⊢ ( 𝑐 = 𝑝 → ( ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 267 |
266
|
ralbidv |
⊢ ( 𝑐 = 𝑝 → ( ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 268 |
267
|
raleqbi1dv |
⊢ ( 𝑐 = 𝑝 → ( ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 269 |
268
|
rabbidv |
⊢ ( 𝑐 = 𝑝 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 270 |
269
|
inteqd |
⊢ ( 𝑐 = 𝑝 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 271 |
270
|
csbeq2dv |
⊢ ( 𝑐 = 𝑝 → ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 272 |
69 271
|
csbie |
⊢ ⦋ 𝑝 / 𝑐 ⦌ ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } |
| 273 |
|
oveq2 |
⊢ ( 𝑑 = 𝑞 → ( 𝑎 𝑤 𝑑 ) = ( 𝑎 𝑤 𝑞 ) ) |
| 274 |
273
|
oveq1d |
⊢ ( 𝑑 = 𝑞 → ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) = ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ) |
| 275 |
274
|
eleq1d |
⊢ ( 𝑑 = 𝑞 → ( ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 276 |
275
|
raleqbi1dv |
⊢ ( 𝑑 = 𝑞 → ( ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 277 |
276
|
ralbidv |
⊢ ( 𝑑 = 𝑞 → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ) ) |
| 278 |
277
|
rabbidv |
⊢ ( 𝑑 = 𝑞 → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 279 |
278
|
inteqd |
⊢ ( 𝑑 = 𝑞 → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 280 |
71 279
|
csbie |
⊢ ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } |
| 281 |
272 280
|
eqtri |
⊢ ⦋ 𝑝 / 𝑐 ⦌ ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } |
| 282 |
|
oveq |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( 𝑎 𝑤 𝑞 ) = ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) ) |
| 283 |
|
oveq |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( 𝑝 𝑤 𝑏 ) = ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) |
| 284 |
282 283
|
oveq12d |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) = ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ) |
| 285 |
|
oveq |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( 𝑎 𝑤 𝑏 ) = ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) |
| 286 |
285
|
oveq2d |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) = ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ) |
| 287 |
284 286
|
eleq12d |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ) ) |
| 288 |
287
|
2ralbidv |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ( ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ) ) |
| 289 |
288
|
rabbidv |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ) |
| 290 |
289
|
inteqd |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 𝑤 𝑞 ) +no ( 𝑝 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ) |
| 291 |
281 290
|
eqtrid |
⊢ ( 𝑤 = ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) → ⦋ 𝑝 / 𝑐 ⦌ ⦋ 𝑞 / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ) |
| 292 |
|
eqid |
⊢ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) |
| 293 |
263 291 292
|
ovmpog |
⊢ ( ( ⟨ 𝑝 , 𝑞 ⟩ ∈ V ∧ ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ∈ V ∧ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ∈ On ) → ( ⟨ 𝑝 , 𝑞 ⟩ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ) |
| 294 |
65 76 259 293
|
mp3an12i |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( ⟨ 𝑝 , 𝑞 ⟩ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑑 ⦌ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑑 ( ( 𝑎 𝑤 𝑑 ) +no ( 𝑐 𝑤 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 𝑤 𝑏 ) ) } ) ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑞 ) +no ( 𝑝 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ( ·no ↾ ( ( suc 𝑝 × suc 𝑞 ) ∖ { ⟨ 𝑝 , 𝑞 ⟩ } ) ) 𝑏 ) ) } ) |
| 295 |
64 294 155
|
3eqtrd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) |
| 296 |
295 258
|
eqeltrd |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( 𝑝 ·no 𝑞 ) ∈ On ) |
| 297 |
296 295
|
jca |
⊢ ( ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) ∧ ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) ) → ( ( 𝑝 ·no 𝑞 ) ∈ On ∧ ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |
| 298 |
297
|
ex |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( 𝑟 ·no 𝑠 ) ∈ On ∧ ∀ 𝑟 ∈ 𝑝 ( 𝑟 ·no 𝑞 ) ∈ On ∧ ∀ 𝑠 ∈ 𝑞 ( 𝑝 ·no 𝑠 ) ∈ On ) → ( ( 𝑝 ·no 𝑞 ) ∈ On ∧ ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 299 |
61 298
|
syl5 |
⊢ ( ( 𝑝 ∈ On ∧ 𝑞 ∈ On ) → ( ( ∀ 𝑟 ∈ 𝑝 ∀ 𝑠 ∈ 𝑞 ( ( 𝑟 ·no 𝑠 ) ∈ On ∧ ( 𝑟 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ∧ ∀ 𝑟 ∈ 𝑝 ( ( 𝑟 ·no 𝑞 ) ∈ On ∧ ( 𝑟 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑟 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑟 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ∧ ∀ 𝑠 ∈ 𝑞 ( ( 𝑝 ·no 𝑠 ) ∈ On ∧ ( 𝑝 ·no 𝑠 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑠 ( ( 𝑎 ·no 𝑠 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) → ( ( 𝑝 ·no 𝑞 ) ∈ On ∧ ( 𝑝 ·no 𝑞 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑞 ( ( 𝑎 ·no 𝑞 ) +no ( 𝑝 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) ) |
| 300 |
11 22 32 43 54 299
|
on2ind |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) ) |