Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝑅 Fr 𝐴 ) |
2 |
|
snssi |
⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 ) |
3 |
2
|
adantl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ⊆ 𝐴 ) |
4 |
|
snnzg |
⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ≠ ∅ ) |
5 |
4
|
adantl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ≠ ∅ ) |
6 |
|
snex |
⊢ { 𝐵 } ∈ V |
7 |
6
|
frc |
⊢ ( ( 𝑅 Fr 𝐴 ∧ { 𝐵 } ⊆ 𝐴 ∧ { 𝐵 } ≠ ∅ ) → ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ) |
8 |
1 3 5 7
|
syl3anc |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ) |
9 |
|
breq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) ) |
10 |
9
|
rabeq0w |
⊢ ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝑦 ) |
11 |
|
breq2 |
⊢ ( 𝑦 = 𝐵 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝐵 ) ) |
12 |
11
|
notbid |
⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑅 𝐵 ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) ) |
14 |
10 13
|
bitrid |
⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) ) |
15 |
14
|
rexsng |
⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ) ) |
16 |
|
breq1 |
⊢ ( 𝑧 = 𝐵 → ( 𝑧 𝑅 𝐵 ↔ 𝐵 𝑅 𝐵 ) ) |
17 |
16
|
notbid |
⊢ ( 𝑧 = 𝐵 → ( ¬ 𝑧 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) ) |
18 |
17
|
ralsng |
⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑧 ∈ { 𝐵 } ¬ 𝑧 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 𝐵 ) ) |
19 |
15 18
|
bitrd |
⊢ ( 𝐵 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ { 𝐵 } { 𝑥 ∈ { 𝐵 } ∣ 𝑥 𝑅 𝑦 } = ∅ ↔ ¬ 𝐵 𝑅 𝐵 ) ) |
21 |
8 20
|
mpbid |
⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐵 𝑅 𝐵 ) |