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 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )