Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑏 ) = ( 𝑐 +no 𝑏 ) ) |
2 |
|
oveq2 |
⊢ ( 𝑎 = 𝑐 → ( 𝑏 +no 𝑎 ) = ( 𝑏 +no 𝑐 ) ) |
3 |
1 2
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ↔ ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ) ) |
4 |
|
oveq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 +no 𝑏 ) = ( 𝑐 +no 𝑑 ) ) |
5 |
|
oveq1 |
⊢ ( 𝑏 = 𝑑 → ( 𝑏 +no 𝑐 ) = ( 𝑑 +no 𝑐 ) ) |
6 |
4 5
|
eqeq12d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ↔ ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ) ) |
7 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 +no 𝑑 ) = ( 𝑐 +no 𝑑 ) ) |
8 |
|
oveq2 |
⊢ ( 𝑎 = 𝑐 → ( 𝑑 +no 𝑎 ) = ( 𝑑 +no 𝑐 ) ) |
9 |
7 8
|
eqeq12d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ↔ ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ) ) |
10 |
|
oveq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no 𝑏 ) = ( 𝐴 +no 𝑏 ) ) |
11 |
|
oveq2 |
⊢ ( 𝑎 = 𝐴 → ( 𝑏 +no 𝑎 ) = ( 𝑏 +no 𝐴 ) ) |
12 |
10 11
|
eqeq12d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ↔ ( 𝐴 +no 𝑏 ) = ( 𝑏 +no 𝐴 ) ) ) |
13 |
|
oveq2 |
⊢ ( 𝑏 = 𝐵 → ( 𝐴 +no 𝑏 ) = ( 𝐴 +no 𝐵 ) ) |
14 |
|
oveq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 +no 𝐴 ) = ( 𝐵 +no 𝐴 ) ) |
15 |
13 14
|
eqeq12d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 +no 𝑏 ) = ( 𝑏 +no 𝐴 ) ↔ ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) ) ) |
16 |
|
eleq1 |
⊢ ( ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
17 |
16
|
ralimi |
⊢ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
18 |
|
ralbi |
⊢ ( ∀ 𝑑 ∈ 𝑏 ( ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
19 |
17 18
|
syl |
⊢ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
20 |
19
|
3ad2ant3 |
⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
21 |
20
|
adantl |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) |
22 |
|
eleq1 |
⊢ ( ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
23 |
22
|
ralimi |
⊢ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
24 |
|
ralbi |
⊢ ( ∀ 𝑐 ∈ 𝑎 ( ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
25 |
23 24
|
syl |
⊢ ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
26 |
25
|
3ad2ant2 |
⊢ ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
27 |
26
|
adantl |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) |
28 |
21 27
|
anbi12d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ) ) ) |
29 |
28
|
biancomd |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) ↔ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) ) ) |
30 |
29
|
rabbidv |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } ) |
31 |
30
|
inteqd |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } ) |
32 |
|
naddov2 |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } ) |
33 |
32
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑎 +no 𝑏 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) ∈ 𝑥 ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) ∈ 𝑥 ) } ) |
34 |
|
naddov2 |
⊢ ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑏 +no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } ) |
35 |
34
|
ancoms |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( 𝑏 +no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } ) |
36 |
35
|
adantr |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑏 +no 𝑎 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝑎 ( 𝑏 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑑 +no 𝑎 ) ∈ 𝑥 ) } ) |
37 |
31 33 36
|
3eqtr4d |
⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) ∧ ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) ) → ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ) |
38 |
37
|
ex |
⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( 𝑐 +no 𝑑 ) = ( 𝑑 +no 𝑐 ) ∧ ∀ 𝑐 ∈ 𝑎 ( 𝑐 +no 𝑏 ) = ( 𝑏 +no 𝑐 ) ∧ ∀ 𝑑 ∈ 𝑏 ( 𝑎 +no 𝑑 ) = ( 𝑑 +no 𝑎 ) ) → ( 𝑎 +no 𝑏 ) = ( 𝑏 +no 𝑎 ) ) ) |
39 |
3 6 9 12 15 38
|
on2ind |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) = ( 𝐵 +no 𝐴 ) ) |