Step |
Hyp |
Ref |
Expression |
1 |
|
pridl.1 |
⊢ 𝐻 = ( 2nd ‘ 𝑅 ) |
2 |
|
eqid |
⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 ) |
4 |
2 1 3
|
ispridl |
⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) ) |
5 |
|
df-3an |
⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) |
6 |
4 5
|
bitrdi |
⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ ran ( 1st ‘ 𝑅 ) ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) ) |
7 |
6
|
simplbda |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
8 |
|
raleq |
⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) |
9 |
|
sseq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝑃 ↔ 𝐴 ⊆ 𝑃 ) ) |
10 |
9
|
orbi1d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) |
11 |
8 10
|
imbi12d |
⊢ ( 𝑎 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ) ) |
12 |
|
raleq |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) |
14 |
|
sseq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ 𝑃 ↔ 𝐵 ⊆ 𝑃 ) ) |
15 |
14
|
orbi2d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ↔ ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) |
16 |
13 15
|
imbi12d |
⊢ ( 𝑏 = 𝐵 → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) ) |
17 |
11 16
|
rspc2v |
⊢ ( ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑎 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) ) |
18 |
7 17
|
syl5com |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) ) |
19 |
18
|
expd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) → ( 𝐴 ∈ ( Idl ‘ 𝑅 ) → ( 𝐵 ∈ ( Idl ‘ 𝑅 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) ) ) ) |
20 |
19
|
3imp2 |
⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( Idl ‘ 𝑅 ) ∧ 𝐵 ∈ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) ) → ( 𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃 ) ) |