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* = ( 𝑎 ∈ V ↦ ∪ 𝑖 ∈ { 0 , 1 } ( 𝑎 ↑𝑟 𝑖 ) )
2 dfrcl4 ⊢ r* = ( 𝑏 ∈ V ↦ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑏 ↑𝑟 𝑗 ) )
3 dfrcl4 ⊢ r* = ( 𝑐 ∈ V ↦ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑐 ↑𝑟 𝑘 ) )
4 prex ⊢ { 0 , 1 } ∈ V
5 unidm ⊢ ( { 0 , 1 } ∪ { 0 , 1 } ) = { 0 , 1 }
6 5 eqcomi ⊢ { 0 , 1 } = ( { 0 , 1 } ∪ { 0 , 1 } )
7 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 𝑗 ) )
8 7 cbviunv ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 )
9 1ex ⊢ 1 ∈ V
10 oveq2 ⊢ ( 𝑖 = 1 → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
11 9 10 iunxsn ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 )
12 ovex ⊢ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
13 4 12 iunex ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ∈ V
14 relexp1g ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ∈ V → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
15 13 14 ax-mp ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 )
16 11 15 eqtri ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 )
17 16 eqcomi ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
18 8 17 eqtri ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
19 snsspr2 ⊢ { 1 } ⊆ { 0 , 1 }
20 iunss1 ⊢ ( { 1 } ⊆ { 0 , 1 } → ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
21 19 20 ax-mp ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
22 18 21 eqsstri ⊢ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
23 0elpr01 ⊢ 0 ∈ { 0 , 1 }
24 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑑 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 0 ) )
25 24 ssiun2s ⊢ ( 0 ∈ { 0 , 1 } → ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) )
26 23 25 ax-mp ⊢ ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
27 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 𝑘 ) )
28 27 cbviunv ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
29 28 eqimssi ⊢ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 )
30 unss12 ⊢ ( ( ( 𝑑 ↑𝑟 0 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∧ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ⊆ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ) )
31 26 29 30 mp2an ⊢ ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) )
32 df-pr ⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } )
33 iuneq1 ⊢ ( { 0 , 1 } = ( { 0 } ∪ { 1 } ) → ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
34 32 33 ax-mp ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
35 iunxun ⊢ ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ∪ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
36 c0ex ⊢ 0 ∈ V
37 oveq2 ⊢ ( 𝑖 = 0 → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) )
38 36 37 iunxsn ⊢ ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 )
39 vex ⊢ 𝑑 ∈ 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 ⊢ ( ( 𝑑 ∈ V ∧ { 0 , 1 } ⊆ ℕ0 ∧ ( { 0 , 1 } ∩ { 0 , 1 } ) ≠ ∅ ) → ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) = ( 𝑑 ↑𝑟 0 ) )
47 39 43 45 46 mp3an ⊢ ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 0 ) = ( 𝑑 ↑𝑟 0 )
48 38 47 eqtri ⊢ ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( 𝑑 ↑𝑟 0 )
49 48 16 uneq12i ⊢ ( ∪ 𝑖 ∈ { 0 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ∪ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
50 35 49 eqtri ⊢ ∪ 𝑖 ∈ ( { 0 } ∪ { 1 } ) ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
51 34 50 eqtri ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ( 𝑑 ↑𝑟 0 ) ∪ ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) )
52 iunxun ⊢ ∪ 𝑘 ∈ ( { 0 , 1 } ∪ { 0 , 1 } ) ( 𝑑 ↑𝑟 𝑘 ) = ( ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) ∪ ∪ 𝑘 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑘 ) )
53 31 51 52 3sstr4i ⊢ ∪ 𝑖 ∈ { 0 , 1 } ( ∪ 𝑗 ∈ { 0 , 1 } ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ( { 0 , 1 } ∪ { 0 , 1 } ) ( 𝑑 ↑𝑟 𝑘 )
54 1 2 3 4 4 6 22 22 53 comptiunov2i ⊢ ( r* ∘ r* ) = r*