This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Jonathan Ben-Naim df-bnj15
Description: Define the following predicate: R is both well-founded and set-like on
A . (Contributed by Jonathan Ben-Naim , 3-Jun-2011)
(New usage is discouraged.)
Ref
Expression
Assertion
df-bnj15 ⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cR ⊢ 𝑅
1
cA ⊢ 𝐴
2
1 0
w-bnj15 ⊢ 𝑅 FrSe 𝐴
3
1 0
wfr ⊢ 𝑅 Fr 𝐴
4
1 0
w-bnj13 ⊢ 𝑅 Se 𝐴
5
3 4
wa ⊢ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 )
6
2 5
wb ⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )