Metamath Proof Explorer

Theorem bnj1154

Description: Property of Fr . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1154 ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 bnj658 ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → R Fr A ∧ B ⊆ A ∧ B ≠ ∅
2 elisset ⊢ B ∈ V → ∃ b b = B
3 2 bnj708 ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → ∃ b b = B
4 df-fr ⊢ R Fr A ↔ ∀ b b ⊆ A ∧ b ≠ ∅ → ∃ x ∈ b ∀ y ∈ b ¬ y R x
5 4 biimpi ⊢ R Fr A → ∀ b b ⊆ A ∧ b ≠ ∅ → ∃ x ∈ b ∀ y ∈ b ¬ y R x
6 5 19.21bi ⊢ R Fr A → b ⊆ A ∧ b ≠ ∅ → ∃ x ∈ b ∀ y ∈ b ¬ y R x
7 6 3impib ⊢ R Fr A ∧ b ⊆ A ∧ b ≠ ∅ → ∃ x ∈ b ∀ y ∈ b ¬ y R x
8 sseq1 ⊢ b = B → b ⊆ A ↔ B ⊆ A
9 neeq1 ⊢ b = B → b ≠ ∅ ↔ B ≠ ∅
10 8 9 3anbi23d ⊢ b = B → R Fr A ∧ b ⊆ A ∧ b ≠ ∅ ↔ R Fr A ∧ B ⊆ A ∧ B ≠ ∅
11 raleq ⊢ b = B → ∀ y ∈ b ¬ y R x ↔ ∀ y ∈ B ¬ y R x
12 11 rexeqbi1dv ⊢ b = B → ∃ x ∈ b ∀ y ∈ b ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x
13 10 12 imbi12d ⊢ b = B → R Fr A ∧ b ⊆ A ∧ b ≠ ∅ → ∃ x ∈ b ∀ y ∈ b ¬ y R x ↔ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
14 7 13 mpbii ⊢ b = B → R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
15 3 14 bnj593 ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → ∃ b R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
16 15 bnj937 ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → R Fr A ∧ B ⊆ A ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
17 1 16 mpd ⊢ R Fr A ∧ B ⊆ A ∧ B ≠ ∅ ∧ B ∈ V → ∃ x ∈ B ∀ y ∈ B ¬ y R x