Step |
Hyp |
Ref |
Expression |
1 |
|
omord2 |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) |
2 |
|
3anrot |
⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ↔ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ) |
3 |
|
omcan |
⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |
4 |
2 3
|
sylanbr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |
5 |
4
|
bicomd |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 = 𝐵 ↔ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) |
6 |
1 5
|
orbi12d |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) ) |
7 |
|
onsseleq |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
8 |
7
|
3adant3 |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
10 |
|
omcl |
⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ·o 𝐴 ) ∈ On ) |
11 |
|
omcl |
⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ·o 𝐵 ) ∈ On ) |
12 |
10 11
|
anim12dan |
⊢ ( ( 𝐶 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) ) |
13 |
12
|
ancoms |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) ) |
14 |
13
|
3impa |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) ) |
15 |
|
onsseleq |
⊢ ( ( ( 𝐶 ·o 𝐴 ) ∈ On ∧ ( 𝐶 ·o 𝐵 ) ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) ) |
16 |
14 15
|
syl |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) ) |
17 |
16
|
adantr |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ∨ ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝐵 ) ) ) ) |
18 |
6 9 17
|
3bitr4d |
⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) ) |