Step |
Hyp |
Ref |
Expression |
1 |
|
frpomin |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
2 |
|
vex |
⊢ 𝑥 ∈ V |
3 |
2
|
dfpred3 |
⊢ Pred ( 𝑅 , 𝐵 , 𝑥 ) = { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } |
4 |
3
|
eqeq1i |
⊢ ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ) |
5 |
|
rabeq0 |
⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
6 |
4 5
|
bitri |
⊢ ( Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
7 |
6
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
8 |
1 7
|
sylibr |
⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 Pred ( 𝑅 , 𝐵 , 𝑥 ) = ∅ ) |