| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oveq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 +no 𝑏 ) = ( 𝑥 +no 𝑏 ) ) |
| 2 |
1
|
oveq1d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ) |
| 3 |
|
oveq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ) |
| 4 |
2 3
|
eqeq12d |
⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) ↔ ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ) ) |
| 5 |
|
oveq2 |
⊢ ( 𝑏 = 𝑦 → ( 𝑥 +no 𝑏 ) = ( 𝑥 +no 𝑦 ) ) |
| 6 |
5
|
oveq1d |
⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) ) |
| 7 |
|
oveq1 |
⊢ ( 𝑏 = 𝑦 → ( 𝑏 +no 𝑐 ) = ( 𝑦 +no 𝑐 ) ) |
| 8 |
7
|
oveq2d |
⊢ ( 𝑏 = 𝑦 → ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ) |
| 9 |
6 8
|
eqeq12d |
⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ↔ ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ) ) |
| 10 |
|
oveq2 |
⊢ ( 𝑐 = 𝑧 → ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) ) |
| 11 |
|
oveq2 |
⊢ ( 𝑐 = 𝑧 → ( 𝑦 +no 𝑐 ) = ( 𝑦 +no 𝑧 ) ) |
| 12 |
11
|
oveq2d |
⊢ ( 𝑐 = 𝑧 → ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) |
| 13 |
10 12
|
eqeq12d |
⊢ ( 𝑐 = 𝑧 → ( ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ↔ ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) ) |
| 14 |
|
oveq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 +no 𝑦 ) = ( 𝑥 +no 𝑦 ) ) |
| 15 |
14
|
oveq1d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) ) |
| 16 |
|
oveq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) |
| 17 |
15 16
|
eqeq12d |
⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ↔ ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) ) |
| 18 |
|
oveq2 |
⊢ ( 𝑏 = 𝑦 → ( 𝑎 +no 𝑏 ) = ( 𝑎 +no 𝑦 ) ) |
| 19 |
18
|
oveq1d |
⊢ ( 𝑏 = 𝑦 → ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) ) |
| 20 |
|
oveq1 |
⊢ ( 𝑏 = 𝑦 → ( 𝑏 +no 𝑧 ) = ( 𝑦 +no 𝑧 ) ) |
| 21 |
20
|
oveq2d |
⊢ ( 𝑏 = 𝑦 → ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ) |
| 22 |
19 21
|
eqeq12d |
⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ↔ ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ) ) |
| 23 |
5
|
oveq1d |
⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) ) |
| 24 |
20
|
oveq2d |
⊢ ( 𝑏 = 𝑦 → ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) |
| 25 |
23 24
|
eqeq12d |
⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ↔ ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ) ) |
| 26 |
|
oveq2 |
⊢ ( 𝑐 = 𝑧 → ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) ) |
| 27 |
11
|
oveq2d |
⊢ ( 𝑐 = 𝑧 → ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ) |
| 28 |
26 27
|
eqeq12d |
⊢ ( 𝑐 = 𝑧 → ( ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ↔ ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ) ) |
| 29 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) ) |
| 30 |
29
|
oveq1d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( ( 𝐴 +no 𝑏 ) +no 𝑐 ) ) |
| 31 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) = ( 𝐴 +no ( 𝑏 +no 𝑐 ) ) ) |
| 32 |
30 31
|
eqeq12d |
⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) ↔ ( ( 𝐴 +no 𝑏 ) +no 𝑐 ) = ( 𝐴 +no ( 𝑏 +no 𝑐 ) ) ) ) |
| 33 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) ) |
| 34 |
33
|
oveq1d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +no 𝑏 ) +no 𝑐 ) = ( ( 𝐴 +no 𝐵 ) +no 𝑐 ) ) |
| 35 |
|
oveq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 +no 𝑐 ) = ( 𝐵 +no 𝑐 ) ) |
| 36 |
35
|
oveq2d |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no ( 𝑏 +no 𝑐 ) ) = ( 𝐴 +no ( 𝐵 +no 𝑐 ) ) ) |
| 37 |
34 36
|
eqeq12d |
⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 +no 𝑏 ) +no 𝑐 ) = ( 𝐴 +no ( 𝑏 +no 𝑐 ) ) ↔ ( ( 𝐴 +no 𝐵 ) +no 𝑐 ) = ( 𝐴 +no ( 𝐵 +no 𝑐 ) ) ) ) |
| 38 |
|
oveq2 |
⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 +no 𝐵 ) +no 𝑐 ) = ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) ) |
| 39 |
|
oveq2 |
⊢ ( 𝑐 = 𝐶 → ( 𝐵 +no 𝑐 ) = ( 𝐵 +no 𝐶 ) ) |
| 40 |
39
|
oveq2d |
⊢ ( 𝑐 = 𝐶 → ( 𝐴 +no ( 𝐵 +no 𝑐 ) ) = ( 𝐴 +no ( 𝐵 +no 𝐶 ) ) ) |
| 41 |
38 40
|
eqeq12d |
⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐴 +no 𝐵 ) +no 𝑐 ) = ( 𝐴 +no ( 𝐵 +no 𝑐 ) ) ↔ ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) = ( 𝐴 +no ( 𝐵 +no 𝐶 ) ) ) ) |
| 42 |
|
simpr21 |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ) |
| 43 |
|
eleq1 |
⊢ ( ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) → ( ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 44 |
43
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) → ∀ 𝑥 ∈ 𝑎 ( ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 45 |
|
ralbi |
⊢ ( ∀ 𝑥 ∈ 𝑎 ( ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ) → ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ↔ ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 46 |
42 44 45
|
3syl |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ↔ ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 47 |
|
simpr23 |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) |
| 48 |
|
eleq1 |
⊢ ( ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) → ( ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 49 |
48
|
ralimi |
⊢ ( ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) → ∀ 𝑦 ∈ 𝑏 ( ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 50 |
|
ralbi |
⊢ ( ∀ 𝑦 ∈ 𝑏 ( ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ) → ( ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ↔ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 51 |
47 49 50
|
3syl |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ↔ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ) ) |
| 52 |
|
simpr3 |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) |
| 53 |
|
eleq1 |
⊢ ( ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) → ( ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) ) |
| 54 |
53
|
ralimi |
⊢ ( ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) → ∀ 𝑧 ∈ 𝑐 ( ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) ) |
| 55 |
|
ralbi |
⊢ ( ∀ 𝑧 ∈ 𝑐 ( ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ↔ ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ↔ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) ) |
| 56 |
52 54 55
|
3syl |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ↔ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) ) |
| 57 |
46 51 56
|
3anbi123d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ) ↔ ( ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) ) ) |
| 58 |
57
|
rabbidv |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ) } = { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) } ) |
| 59 |
58
|
inteqd |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ) } = ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) } ) |
| 60 |
|
naddasslem1 |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ) } ) |
| 61 |
60
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) ∈ 𝑤 ) } ) |
| 62 |
|
naddasslem2 |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) = ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) } ) |
| 63 |
62
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) = ∩ { 𝑤 ∈ On ∣ ( ∀ 𝑥 ∈ 𝑎 ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑦 ∈ 𝑏 ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ∈ 𝑤 ∧ ∀ 𝑧 ∈ 𝑐 ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ∈ 𝑤 ) } ) |
| 64 |
59 61 63
|
3eqtr4d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) ∧ ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) ) → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) ) |
| 65 |
64
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On ) → ( ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑦 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 +no 𝑦 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑦 +no 𝑐 ) ) ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑧 ∈ 𝑐 ( ( 𝑥 +no 𝑏 ) +no 𝑧 ) = ( 𝑥 +no ( 𝑏 +no 𝑧 ) ) ) ∧ ( ∀ 𝑥 ∈ 𝑎 ( ( 𝑥 +no 𝑏 ) +no 𝑐 ) = ( 𝑥 +no ( 𝑏 +no 𝑐 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑦 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑦 +no 𝑧 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ( ( 𝑎 +no 𝑦 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑦 +no 𝑐 ) ) ) ∧ ∀ 𝑧 ∈ 𝑐 ( ( 𝑎 +no 𝑏 ) +no 𝑧 ) = ( 𝑎 +no ( 𝑏 +no 𝑧 ) ) ) → ( ( 𝑎 +no 𝑏 ) +no 𝑐 ) = ( 𝑎 +no ( 𝑏 +no 𝑐 ) ) ) ) |
| 66 |
4 9 13 17 22 25 28 32 37 41 65
|
on3ind |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) = ( 𝐴 +no ( 𝐵 +no 𝐶 ) ) ) |