Metamath Proof Explorer

Theorem lrrecpred

Description: Finally, we calculate the value of the predecessor class over R . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
Assertion lrrecpred ⊢ A ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A

Proof

Step Hyp Ref Expression
1 lrrec.1 ⊢ R = x y | x ∈ L ⁡ y ∪ R ⁡ y
2 dfpred3g ⊢ A ∈ No → Pred R No A = b ∈ No | b R A
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 5 9 eqtrdi ⊢ A ∈ No → b ∈ No | b R A = L ⁡ A ∪ R ⁡ A ∩ No
11 leftssold ⊢ A ∈ No → L ⁡ A ⊆ Old ⁡ bday ⁡ A
12 bdayelon ⊢ bday ⁡ A ∈ On
13 oldf ⊢ Old : On ⟶ 𝒫 No
14 13 ffvelrni ⊢ bday ⁡ A ∈ On → Old ⁡ bday ⁡ A ∈ 𝒫 No
15 14 elpwid ⊢ bday ⁡ A ∈ On → Old ⁡ bday ⁡ A ⊆ No
16 12 15 ax-mp ⊢ Old ⁡ bday ⁡ A ⊆ No
17 11 16 sstrdi ⊢ A ∈ No → L ⁡ A ⊆ No
18 rightssold ⊢ A ∈ No → R ⁡ A ⊆ Old ⁡ bday ⁡ A
19 18 16 sstrdi ⊢ A ∈ No → R ⁡ A ⊆ No
20 17 19 unssd ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A ⊆ No
21 df-ss ⊢ L ⁡ A ∪ R ⁡ A ⊆ No ↔ L ⁡ A ∪ R ⁡ A ∩ No = L ⁡ A ∪ R ⁡ A
22 20 21 sylib ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A ∩ No = L ⁡ A ∪ R ⁡ A
23 2 10 22 3eqtrd ⊢ A ∈ No → Pred R No A = L ⁡ A ∪ R ⁡ A