Metamath Proof Explorer

Theorem rtrclexi

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

Ref Expression
Hypothesis rtrclexi.1 ⊢ 𝐴 ∈ 𝑉
Assertion rtrclexi ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V

Proof

Step Hyp Ref Expression
1 rtrclexi.1 ⊢ 𝐴 ∈ 𝑉
2 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
3 coundir ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
4 coundi ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
5 cossxp ⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
6 ssun1 ⊢ dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
7 ssun2 ⊢ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
8 xpss12 ⊢ ( ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
9 6 7 8 mp2an ⊢ ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
10 5 9 sstri ⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
11 cossxp ⊢ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 )
12 dmxpss ⊢ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
13 xpss12 ⊢ ( ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
14 12 7 13 mp2an ⊢ ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
15 11 14 sstri ⊢ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
16 10 15 unssi ⊢ ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
17 4 16 eqsstri ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
18 coundi ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
19 cossxp ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
20 rnxpss ⊢ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
21 xpss12 ⊢ ( ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
22 6 20 21 mp2an ⊢ ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
23 19 22 sstri ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
24 xpidtr ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
25 23 24 unssi ⊢ ( ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
26 18 25 eqsstri ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
27 17 26 unssi ⊢ ( ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
28 3 27 eqsstri ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
29 ssun2 ⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
30 28 29 sstri ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
31 dmun ⊢ dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
32 6 12 unssi ⊢ ( dom 𝐴 ∪ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
33 31 32 eqsstri ⊢ dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
34 rnun ⊢ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( ran 𝐴 ∪ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
35 7 20 unssi ⊢ ( ran 𝐴 ∪ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
36 34 35 eqsstri ⊢ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
37 33 36 unssi ⊢ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
38 ssres2 ⊢ ( ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 ) → ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
39 37 38 ax-mp ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) )
40 idssxp ⊢ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
41 39 40 sstri ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
42 41 29 sstri ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
43 id ⊢ ( ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) → ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
44 30 42 43 mp2an ⊢ ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
45 1 elexi ⊢ 𝐴 ∈ V
46 45 dmex ⊢ dom 𝐴 ∈ V
47 45 rnex ⊢ ran 𝐴 ∈ V
48 46 47 unex ⊢ ( dom 𝐴 ∪ ran 𝐴 ) ∈ V
49 48 48 xpex ⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∈ V
50 45 49 unex ⊢ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∈ V
51 id ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
52 51 51 coeq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( 𝑥 ∘ 𝑥 ) = ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
53 52 51 sseq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ↔ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
54 dmeq ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → dom 𝑥 = dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
55 rneq ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ran 𝑥 = ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
56 54 55 uneq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( dom 𝑥 ∪ ran 𝑥 ) = ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
57 56 reseq2d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
58 57 51 sseq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ↔ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
59 53 58 anbi12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ↔ ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
60 59 cleq2lem ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) ↔ ( 𝐴 ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ) )
61 50 60 spcev ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) )
62 intexab ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V )
63 61 62 sylib ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V )
64 2 44 63 mp2an ⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V