Description: Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 19-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frc.1 | ⊢ 𝐵 ∈ V | |
Assertion | frc | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frc.1 | ⊢ 𝐵 ∈ V | |
2 | fri | ⊢ ( ( ( 𝐵 ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) | |
3 | 1 2 | mpanl1 | ⊢ ( ( 𝑅 Fr 𝐴 ∧ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
4 | 3 | 3impb | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
5 | rabeq0 | ⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) | |
6 | 5 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐵 { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) |
7 | 4 6 | sylibr | ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 { 𝑦 ∈ 𝐵 ∣ 𝑦 𝑅 𝑥 } = ∅ ) |