This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 bnj658 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) )
2 elisset ⊢ ( 𝐵 ∈ V → ∃ 𝑏 𝑏 = 𝐵 )
3 2 bnj708 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ∃ 𝑏 𝑏 = 𝐵 )
4 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑏 ( ( 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ) )
5 4 biimpi ⊢ ( 𝑅 Fr 𝐴 → ∀ 𝑏 ( ( 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ) )
6 5 19.21bi ⊢ ( 𝑅 Fr 𝐴 → ( ( 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ) )
7 6 3impib ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 )
8 sseq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
9 neeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
10 8 9 3anbi23d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑅 Fr 𝐴 ∧ 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) ↔ ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) ) )
11 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
12 11 rexeqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 10 12 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑅 Fr 𝐴 ∧ 𝑏 ⊆ 𝐴 ∧ 𝑏 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) ) )
14 7 13 mpbii ⊢ ( 𝑏 = 𝐵 → ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
15 3 14 bnj593 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ∃ 𝑏 ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
16 15 bnj937 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
17 1 16 mpd ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )