Metamath Proof Explorer

Theorem trclublem

Description: If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020)

Ref Expression
Assertion trclublem ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 trclexlem ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V )
2 ssun1 ⊢ 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
3 relcnv ⊢ Rel ◡ 𝑅
4 relssdmrn ⊢ ( Rel ◡ 𝑅 → ◡ 𝑅 ⊆ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) )
5 3 4 ax-mp ⊢ ◡ 𝑅 ⊆ ( dom ◡ 𝑅 × ran ◡ 𝑅 )
6 ssequn1 ⊢ ( ◡ 𝑅 ⊆ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) ↔ ( ◡ 𝑅 ∪ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) ) = ( dom ◡ 𝑅 × ran ◡ 𝑅 ) )
7 5 6 mpbi ⊢ ( ◡ 𝑅 ∪ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) ) = ( dom ◡ 𝑅 × ran ◡ 𝑅 )
8 cnvun ⊢ ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( ◡ 𝑅 ∪ ◡ ( dom 𝑅 × ran 𝑅 ) )
9 cnvxp ⊢ ◡ ( dom 𝑅 × ran 𝑅 ) = ( ran 𝑅 × dom 𝑅 )
10 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
11 dfdm4 ⊢ dom 𝑅 = ran ◡ 𝑅
12 10 11 xpeq12i ⊢ ( ran 𝑅 × dom 𝑅 ) = ( dom ◡ 𝑅 × ran ◡ 𝑅 )
13 9 12 eqtri ⊢ ◡ ( dom 𝑅 × ran 𝑅 ) = ( dom ◡ 𝑅 × ran ◡ 𝑅 )
14 13 uneq2i ⊢ ( ◡ 𝑅 ∪ ◡ ( dom 𝑅 × ran 𝑅 ) ) = ( ◡ 𝑅 ∪ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) )
15 8 14 eqtri ⊢ ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( ◡ 𝑅 ∪ ( dom ◡ 𝑅 × ran ◡ 𝑅 ) )
16 7 15 13 3eqtr4i ⊢ ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ◡ ( dom 𝑅 × ran 𝑅 )
17 16 breqi ⊢ ( 𝑏 ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑎 ↔ 𝑏 ◡ ( dom 𝑅 × ran 𝑅 ) 𝑎 )
18 vex ⊢ 𝑏 ∈ V
19 vex ⊢ 𝑎 ∈ V
20 18 19 brcnv ⊢ ( 𝑏 ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑎 ↔ 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 )
21 18 19 brcnv ⊢ ( 𝑏 ◡ ( dom 𝑅 × ran 𝑅 ) 𝑎 ↔ 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 )
22 17 20 21 3bitr3i ⊢ ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ↔ 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 )
23 16 breqi ⊢ ( 𝑐 ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ↔ 𝑐 ◡ ( dom 𝑅 × ran 𝑅 ) 𝑏 )
24 vex ⊢ 𝑐 ∈ V
25 24 18 brcnv ⊢ ( 𝑐 ◡ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ↔ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 )
26 24 18 brcnv ⊢ ( 𝑐 ◡ ( dom 𝑅 × ran 𝑅 ) 𝑏 ↔ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 )
27 23 25 26 3bitr3i ⊢ ( 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ↔ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 )
28 22 27 anbi12i ⊢ ( ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ∧ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ) ↔ ( 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 ∧ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 ) )
29 28 biimpi ⊢ ( ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ∧ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ) → ( 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 ∧ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 ) )
30 29 eximi ⊢ ( ∃ 𝑏 ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ∧ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ) → ∃ 𝑏 ( 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 ∧ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 ) )
31 30 ssopab2i ⊢ { ⟨ 𝑎 , 𝑐 ⟩ ∣ ∃ 𝑏 ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ∧ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ) } ⊆ { ⟨ 𝑎 , 𝑐 ⟩ ∣ ∃ 𝑏 ( 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 ∧ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 ) }
32 df-co ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = { ⟨ 𝑎 , 𝑐 ⟩ ∣ ∃ 𝑏 ( 𝑎 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑏 ∧ 𝑏 ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) 𝑐 ) }
33 df-co ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) = { ⟨ 𝑎 , 𝑐 ⟩ ∣ ∃ 𝑏 ( 𝑎 ( dom 𝑅 × ran 𝑅 ) 𝑏 ∧ 𝑏 ( dom 𝑅 × ran 𝑅 ) 𝑐 ) }
34 31 32 33 3sstr4i ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) )
35 xptrrel ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( dom 𝑅 × ran 𝑅 )
36 ssun2 ⊢ ( dom 𝑅 × ran 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
37 35 36 sstri ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
38 34 37 sstri ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
39 trcleq2lem ⊢ ( 𝑥 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → ( ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ↔ ( 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∧ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ) )
40 39 elabg ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ↔ ( 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∧ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ) )
41 40 biimprd ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V → ( ( 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∧ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ) )
42 2 38 41 mp2ani ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
43 1 42 syl ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )