Metamath Proof Explorer

Theorem corclrcl

Description: The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion corclrcl ⊢ r* ∘ r* = r*

Proof

Step Hyp Ref Expression
1 dfrcl4 ⊢ r* = a ∈ V ⟼ ⋃ i ∈ 0 1 a ↑ r i
2 dfrcl4 ⊢ r* = b ∈ V ⟼ ⋃ j ∈ 0 1 b ↑ r j
3 dfrcl4 ⊢ r* = c ∈ V ⟼ ⋃ k ∈ 0 1 c ↑ r k
4 prex ⊢ 0 1 ∈ V
5 unidm ⊢ 0 1 ∪ 0 1 = 0 1
6 5 eqcomi ⊢ 0 1 = 0 1 ∪ 0 1
7 oveq2 ⊢ k = j → d ↑ r k = d ↑ r j
8 7 cbviunv ⊢ ⋃ k ∈ 0 1 d ↑ r k = ⋃ j ∈ 0 1 d ↑ r j
9 1ex ⊢ 1 ∈ V
10 oveq2 ⊢ i = 1 → ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ j ∈ 0 1 d ↑ r j ↑ r 1
11 9 10 iunxsn ⊢ ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ j ∈ 0 1 d ↑ r j ↑ r 1
12 ovex ⊢ d ↑ r j ∈ V
13 4 12 iunex ⊢ ⋃ j ∈ 0 1 d ↑ r j ∈ V
14 relexp1g ⊢ ⋃ j ∈ 0 1 d ↑ r j ∈ V → ⋃ j ∈ 0 1 d ↑ r j ↑ r 1 = ⋃ j ∈ 0 1 d ↑ r j
15 13 14 ax-mp ⊢ ⋃ j ∈ 0 1 d ↑ r j ↑ r 1 = ⋃ j ∈ 0 1 d ↑ r j
16 11 15 eqtri ⊢ ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ j ∈ 0 1 d ↑ r j
17 16 eqcomi ⊢ ⋃ j ∈ 0 1 d ↑ r j = ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
18 8 17 eqtri ⊢ ⋃ k ∈ 0 1 d ↑ r k = ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
19 snsspr2 ⊢ 1 ⊆ 0 1
20 iunss1 ⊢ 1 ⊆ 0 1 → ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i ⊆ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
21 19 20 ax-mp ⊢ ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i ⊆ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
22 18 21 eqsstri ⊢ ⋃ k ∈ 0 1 d ↑ r k ⊆ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
23 0elpr01 ⊢ 0 ∈ 0 1
24 oveq2 ⊢ k = 0 → d ↑ r k = d ↑ r 0
25 24 ssiun2s ⊢ 0 ∈ 0 1 → d ↑ r 0 ⊆ ⋃ k ∈ 0 1 d ↑ r k
26 23 25 ax-mp ⊢ d ↑ r 0 ⊆ ⋃ k ∈ 0 1 d ↑ r k
27 oveq2 ⊢ j = k → d ↑ r j = d ↑ r k
28 27 cbviunv ⊢ ⋃ j ∈ 0 1 d ↑ r j = ⋃ k ∈ 0 1 d ↑ r k
29 28 eqimssi ⊢ ⋃ j ∈ 0 1 d ↑ r j ⊆ ⋃ k ∈ 0 1 d ↑ r k
30 unss12 ⊢ d ↑ r 0 ⊆ ⋃ k ∈ 0 1 d ↑ r k ∧ ⋃ j ∈ 0 1 d ↑ r j ⊆ ⋃ k ∈ 0 1 d ↑ r k → d ↑ r 0 ∪ ⋃ j ∈ 0 1 d ↑ r j ⊆ ⋃ k ∈ 0 1 d ↑ r k ∪ ⋃ k ∈ 0 1 d ↑ r k
31 26 29 30 mp2an ⊢ d ↑ r 0 ∪ ⋃ j ∈ 0 1 d ↑ r j ⊆ ⋃ k ∈ 0 1 d ↑ r k ∪ ⋃ k ∈ 0 1 d ↑ r k
32 df-pr ⊢ 0 1 = 0 ∪ 1
33 iuneq1 ⊢ 0 1 = 0 ∪ 1 → ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ i ∈ 0 ∪ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
34 32 33 ax-mp ⊢ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ i ∈ 0 ∪ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
35 iunxun ⊢ ⋃ i ∈ 0 ∪ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ i ∈ 0 ⋃ j ∈ 0 1 d ↑ r j ↑ r i ∪ ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i
36 c0ex ⊢ 0 ∈ V
37 oveq2 ⊢ i = 0 → ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ j ∈ 0 1 d ↑ r j ↑ r 0
38 36 37 iunxsn ⊢ ⋃ i ∈ 0 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = ⋃ j ∈ 0 1 d ↑ r j ↑ r 0
39 vex ⊢ d ∈ V
40 0nn0 ⊢ 0 ∈ ℕ 0
41 1nn0 ⊢ 1 ∈ ℕ 0
42 prssi ⊢ 0 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → 0 1 ⊆ ℕ 0
43 40 41 42 mp2an ⊢ 0 1 ⊆ ℕ 0
44 23 23 elini ⊢ 0 ∈ 0 1 ∩ 0 1
45 44 ne0ii ⊢ 0 1 ∩ 0 1 ≠ ∅
46 iunrelexp0 ⊢ d ∈ V ∧ 0 1 ⊆ ℕ 0 ∧ 0 1 ∩ 0 1 ≠ ∅ → ⋃ j ∈ 0 1 d ↑ r j ↑ r 0 = d ↑ r 0
47 39 43 45 46 mp3an ⊢ ⋃ j ∈ 0 1 d ↑ r j ↑ r 0 = d ↑ r 0
48 38 47 eqtri ⊢ ⋃ i ∈ 0 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = d ↑ r 0
49 48 16 uneq12i ⊢ ⋃ i ∈ 0 ⋃ j ∈ 0 1 d ↑ r j ↑ r i ∪ ⋃ i ∈ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = d ↑ r 0 ∪ ⋃ j ∈ 0 1 d ↑ r j
50 35 49 eqtri ⊢ ⋃ i ∈ 0 ∪ 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = d ↑ r 0 ∪ ⋃ j ∈ 0 1 d ↑ r j
51 34 50 eqtri ⊢ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i = d ↑ r 0 ∪ ⋃ j ∈ 0 1 d ↑ r j
52 iunxun ⊢ ⋃ k ∈ 0 1 ∪ 0 1 d ↑ r k = ⋃ k ∈ 0 1 d ↑ r k ∪ ⋃ k ∈ 0 1 d ↑ r k
53 31 51 52 3sstr4i ⊢ ⋃ i ∈ 0 1 ⋃ j ∈ 0 1 d ↑ r j ↑ r i ⊆ ⋃ k ∈ 0 1 ∪ 0 1 d ↑ r k
54 1 2 3 4 4 6 22 22 53 comptiunov2i ⊢ r* ∘ r* = r*