Metamath Proof Explorer

Theorem lrrecse

Description: Next, we show that R is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
Assertion lrrecse ⊢ R Se No

Proof

Step Hyp Ref Expression
1 lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
2 df-se ⊢ R Se No ↔ ∀ a ∈ No b ∈ No | b R a ∈ V
3 1 lrrecval ⊢ b ∈ No ∧ a ∈ No → b R a ↔ b ∈ L ⁡ a ∪ R ⁡ a
4 3 ancoms ⊢ a ∈ No ∧ b ∈ No → b R a ↔ b ∈ L ⁡ a ∪ R ⁡ a
5 4 rabbidva ⊢ a ∈ No → b ∈ No | b R a = b ∈ No | b ∈ L ⁡ a ∪ R ⁡ a
6 dfrab2 ⊢ b ∈ No | b ∈ L ⁡ a ∪ R ⁡ a = b | b ∈ L ⁡ a ∪ R ⁡ a ∩ No
7 abid2 ⊢ b | b ∈ L ⁡ a ∪ R ⁡ a = L ⁡ a ∪ R ⁡ a
8 7 ineq1i ⊢ b | b ∈ L ⁡ a ∪ R ⁡ a ∩ No = L ⁡ a ∪ R ⁡ a ∩ No
9 6 8 eqtri ⊢ b ∈ No | b ∈ L ⁡ a ∪ R ⁡ a = L ⁡ a ∪ R ⁡ a ∩ No
10 fvex ⊢ L ⁡ a ∈ V
11 fvex ⊢ R ⁡ a ∈ V
12 10 11 unex ⊢ L ⁡ a ∪ R ⁡ a ∈ V
13 12 inex1 ⊢ L ⁡ a ∪ R ⁡ a ∩ No ∈ V
14 9 13 eqeltri ⊢ b ∈ No | b ∈ L ⁡ a ∪ R ⁡ a ∈ V
15 5 14 eqeltrdi ⊢ a ∈ No → b ∈ No | b R a ∈ V
16 2 15 mprgbir ⊢ R Se No