Metamath Proof Explorer

Theorem rtrclex

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

Ref Expression
Assertion rtrclex ( 𝐴 ∈ V ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V )

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
2 coundir ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
3 coundi ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
4 cossxp ⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
5 ssun1 ⊢ dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
6 ssun2 ⊢ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
7 xpss12 ⊢ ( ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
8 5 6 7 mp2an ⊢ ( dom 𝐴 × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
9 4 8 sstri ⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
10 cossxp ⊢ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 )
11 dmxpss ⊢ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
12 xpss12 ⊢ ( ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
13 11 6 12 mp2an ⊢ ( dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) × ran 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
14 10 13 sstri ⊢ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
15 9 14 unssi ⊢ ( ( 𝐴 ∘ 𝐴 ) ∪ ( 𝐴 ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
16 3 15 eqsstri ⊢ ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
17 coundi ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
18 cossxp ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
19 rnxpss ⊢ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 )
20 xpss12 ⊢ ( ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ∧ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ) → ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
21 5 19 20 mp2an ⊢ ( dom 𝐴 × ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
22 18 21 sstri ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
23 xpidtr ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
24 22 23 unssi ⊢ ( ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ 𝐴 ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
25 17 24 eqsstri ⊢ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
26 16 25 unssi ⊢ ( ( 𝐴 ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ∪ ( ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
27 2 26 eqsstri ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
28 ssun2 ⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
29 27 28 sstri ⊢ ( ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∘ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
30 dmun ⊢ dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
31 dmxpid ⊢ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
32 31 uneq2i ⊢ ( dom 𝐴 ∪ dom ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
33 ssequn1 ⊢ ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ↔ ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 ) )
34 5 33 mpbi ⊢ ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
35 30 32 34 3eqtri ⊢ dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
36 rnun ⊢ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( ran 𝐴 ∪ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
37 rnxpid ⊢ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
38 37 uneq2i ⊢ ( ran 𝐴 ∪ ran ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
39 ssequn1 ⊢ ( ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ↔ ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 ) )
40 6 39 mpbi ⊢ ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
41 36 38 40 3eqtri ⊢ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
42 35 41 uneq12i ⊢ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( dom 𝐴 ∪ ran 𝐴 ) ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
43 unidm ⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
44 42 43 eqtri ⊢ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
45 44 reseq2i ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) )
46 idssxp ⊢ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
47 45 46 eqsstri ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) )
48 47 28 sstri ⊢ ( I ↾ ( dom ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( ( dom 𝐴 ∪ ran 𝐴 ) × ( dom 𝐴 ∪ ran 𝐴 ) ) )
49 29 48 pm3.2i ⊢ ( ( ( 𝐴 ∪ ( ( 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 𝐴 ) ) ) )
50 rtrclexlem ⊢ ( 𝐴 ∈ V → ( 𝐴 ∪ ( ( 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 60 biimprd ⊢ ( 𝑥 = ( 𝐴 ∪ ( ( 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 𝐴 ) ) ) ) ) → ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) ) )
62 61 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 = ( 𝐴 ∪ ( ( 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 𝐴 ) ) ) ) ) → ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) ) )
63 50 62 spcimedv ⊢ ( 𝐴 ∈ V → ( ( 𝐴 ⊆ ( 𝐴 ∪ ( ( 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 𝑥 ) ) ⊆ 𝑥 ) ) ) )
64 1 49 63 mp2ani ⊢ ( 𝐴 ∈ V → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) )
65 exsimpl ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) → ∃ 𝑥 𝐴 ⊆ 𝑥 )
66 vex ⊢ 𝑥 ∈ V
67 66 ssex ⊢ ( 𝐴 ⊆ 𝑥 → 𝐴 ∈ V )
68 67 exlimiv ⊢ ( ∃ 𝑥 𝐴 ⊆ 𝑥 → 𝐴 ∈ V )
69 65 68 syl ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) → 𝐴 ∈ V )
70 64 69 impbii ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) )
71 intexab ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V )
72 70 71 bitri ⊢ ( 𝐴 ∈ V ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ) } ∈ V )