Metamath Proof Explorer

Theorem trclexi

Description: The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020)

Ref Expression
Hypothesis trclexi.1 ⊢ 𝐴 ∈ 𝑉
Assertion trclexi ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V

Proof

Step Hyp Ref Expression
1 trclexi.1 ⊢ 𝐴 ∈ 𝑉
2 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) )
3 coundir ⊢ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) = ( ( 𝐴 ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ∪ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) )
4 coundi ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) = ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( dom 𝐴 × ran 𝐴 ) ) )
5 cossxp ⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
6 cossxp ⊢ ( 𝐴 ∘ ( dom 𝐴 × ran 𝐴 ) ) ⊆ ( dom ( dom 𝐴 × ran 𝐴 ) × ran 𝐴 )
7 dmxpss ⊢ dom ( dom 𝐴 × ran 𝐴 ) ⊆ dom 𝐴
8 xpss1 ⊢ ( dom ( dom 𝐴 × ran 𝐴 ) ⊆ dom 𝐴 → ( dom ( dom 𝐴 × ran 𝐴 ) × ran 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 ) )
9 7 8 ax-mp ⊢ ( dom ( dom 𝐴 × ran 𝐴 ) × ran 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
10 6 9 sstri ⊢ ( 𝐴 ∘ ( dom 𝐴 × ran 𝐴 ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
11 5 10 unssi ⊢ ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
12 4 11 eqsstri ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
13 coundi ⊢ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) = ( ( ( dom 𝐴 × ran 𝐴 ) ∘ 𝐴 ) ∪ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( dom 𝐴 × ran 𝐴 ) ) )
14 cossxp ⊢ ( ( dom 𝐴 × ran 𝐴 ) ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran ( dom 𝐴 × ran 𝐴 ) )
15 rnxpss ⊢ ran ( dom 𝐴 × ran 𝐴 ) ⊆ ran 𝐴
16 xpss2 ⊢ ( ran ( dom 𝐴 × ran 𝐴 ) ⊆ ran 𝐴 → ( dom 𝐴 × ran ( dom 𝐴 × ran 𝐴 ) ) ⊆ ( dom 𝐴 × ran 𝐴 ) )
17 15 16 ax-mp ⊢ ( dom 𝐴 × ran ( dom 𝐴 × ran 𝐴 ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
18 14 17 sstri ⊢ ( ( dom 𝐴 × ran 𝐴 ) ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
19 xptrrel ⊢ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( dom 𝐴 × ran 𝐴 ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
20 18 19 unssi ⊢ ( ( ( dom 𝐴 × ran 𝐴 ) ∘ 𝐴 ) ∪ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
21 13 20 eqsstri ⊢ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
22 12 21 unssi ⊢ ( ( 𝐴 ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ∪ ( ( dom 𝐴 × ran 𝐴 ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
23 3 22 eqsstri ⊢ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( dom 𝐴 × ran 𝐴 )
24 ssun2 ⊢ ( dom 𝐴 × ran 𝐴 ) ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) )
25 23 24 sstri ⊢ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) )
26 1 elexi ⊢ 𝐴 ∈ V
27 26 dmex ⊢ dom 𝐴 ∈ V
28 26 rnex ⊢ ran 𝐴 ∈ V
29 27 28 xpex ⊢ ( dom 𝐴 × ran 𝐴 ) ∈ V
30 26 29 unex ⊢ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∈ V
31 trcleq2lem ⊢ ( 𝑥 = ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) → ( ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ↔ ( 𝐴 ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∧ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ) )
32 30 31 spcev ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∧ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
33 intexab ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V )
34 32 33 sylib ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∧ ( ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) ⊆ ( 𝐴 ∪ ( dom 𝐴 × ran 𝐴 ) ) ) → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V )
35 2 25 34 mp2an ⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V