Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rtrclex Structured version   Visualization version   GIF version

Theorem rtrclex 40315
 Description: The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.)
Assertion
Ref Expression
rtrclex (𝐴 ∈ V ↔ {𝑥 ∣ (𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
Distinct variable group:   𝑥,𝐴

Proof of Theorem rtrclex
StepHypRef Expression
1 ssun1 4099 . . . 4 𝐴 ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2 coundir 6068 . . . . . . 7 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
3 coundi 6067 . . . . . . . . 9 (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
4 cossxp 6091 . . . . . . . . . . 11 (𝐴𝐴) ⊆ (dom 𝐴 × ran 𝐴)
5 ssun1 4099 . . . . . . . . . . . 12 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
6 ssun2 4100 . . . . . . . . . . . 12 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
7 xpss12 5534 . . . . . . . . . . . 12 ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
85, 6, 7mp2an 691 . . . . . . . . . . 11 (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
94, 8sstri 3924 . . . . . . . . . 10 (𝐴𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
10 cossxp 6091 . . . . . . . . . . 11 (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴)
11 dmxpss 5995 . . . . . . . . . . . 12 dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
12 xpss12 5534 . . . . . . . . . . . 12 ((dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
1311, 6, 12mp2an 691 . . . . . . . . . . 11 (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
1410, 13sstri 3924 . . . . . . . . . 10 (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
159, 14unssi 4112 . . . . . . . . 9 ((𝐴𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
163, 15eqsstri 3949 . . . . . . . 8 (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
17 coundi 6067 . . . . . . . . 9 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
18 cossxp 6091 . . . . . . . . . . 11 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
19 rnxpss 5996 . . . . . . . . . . . 12 ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
20 xpss12 5534 . . . . . . . . . . . 12 ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
215, 19, 20mp2an 691 . . . . . . . . . . 11 (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2218, 21sstri 3924 . . . . . . . . . 10 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
23 xpidtr 5949 . . . . . . . . . 10 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2422, 23unssi 4112 . . . . . . . . 9 ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2517, 24eqsstri 3949 . . . . . . . 8 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2616, 25unssi 4112 . . . . . . 7 ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
272, 26eqsstri 3949 . . . . . 6 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
28 ssun2 4100 . . . . . 6 ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2927, 28sstri 3924 . . . . 5 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
30 dmun 5743 . . . . . . . . . . 11 dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
31 dmxpid 5764 . . . . . . . . . . . 12 dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3231uneq2i 4087 . . . . . . . . . . 11 (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
33 ssequn1 4107 . . . . . . . . . . . 12 (dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
345, 33mpbi 233 . . . . . . . . . . 11 (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3530, 32, 343eqtri 2825 . . . . . . . . . 10 dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
36 rnun 5971 . . . . . . . . . . 11 ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
37 rnxpid 5997 . . . . . . . . . . . 12 ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3837uneq2i 4087 . . . . . . . . . . 11 (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
39 ssequn1 4107 . . . . . . . . . . . 12 (ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
406, 39mpbi 233 . . . . . . . . . . 11 (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
4136, 38, 403eqtri 2825 . . . . . . . . . 10 ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
4235, 41uneq12i 4088 . . . . . . . . 9 (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴))
43 unidm 4079 . . . . . . . . 9 ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
4442, 43eqtri 2821 . . . . . . . 8 (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = (dom 𝐴 ∪ ran 𝐴)
4544reseq2i 5815 . . . . . . 7 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) = ( I ↾ (dom 𝐴 ∪ ran 𝐴))
46 idssxp 5883 . . . . . . 7 ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
4745, 46eqsstri 3949 . . . . . 6 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
4847, 28sstri 3924 . . . . 5 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
4929, 48pm3.2i 474 . . . 4 (((𝐴 ∪ ((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 40314 . . . . 5 (𝐴 ∈ V → (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∈ V)
51 id 22 . . . . . . . . . . 11 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → 𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
5251, 51coeq12d 5699 . . . . . . . . . 10 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (𝑥𝑥) = ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
5352, 51sseq12d 3948 . . . . . . . . 9 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
54 dmeq 5736 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → dom 𝑥 = dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
55 rneq 5770 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ran 𝑥 = ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
5654, 55uneq12d 4091 . . . . . . . . . . 11 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
5756reseq2d 5818 . . . . . . . . . 10 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))))
5857, 51sseq12d 3948 . . . . . . . . 9 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
5953, 58anbi12d 633 . . . . . . . 8 (𝑥 = (𝐴 ∪ ((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 𝐴))))))
6059cleq2lem 40306 . . . . . . 7 (𝑥 = (𝐴 ∪ ((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 𝐴)))))))
6160biimprd 251 . . . . . 6 (𝑥 = (𝐴 ∪ ((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 𝑥)) ⊆ 𝑥))))
6261adantl 485 . . . . 5 ((𝐴 ∈ 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 𝑥)) ⊆ 𝑥))))
6350, 62spcimedv 3542 . . . 4 (𝐴 ∈ 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 𝑥)) ⊆ 𝑥))))
641, 49, 63mp2ani 697 . . 3 (𝐴 ∈ V → ∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
65 exsimpl 1869 . . . 4 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → ∃𝑥 𝐴𝑥)
66 vex 3444 . . . . . 6 𝑥 ∈ V
6766ssex 5189 . . . . 5 (𝐴𝑥𝐴 ∈ V)
6867exlimiv 1931 . . . 4 (∃𝑥 𝐴𝑥𝐴 ∈ V)
6965, 68syl 17 . . 3 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → 𝐴 ∈ V)
7064, 69impbii 212 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
71 intexab 5206 . 2 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) ↔ {𝑥 ∣ (𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
7270, 71bitri 278 1 (𝐴 ∈ V ↔ {𝑥 ∣ (𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∩ cint 4838   I cid 5424   × cxp 5517  dom cdm 5519  ran crn 5520   ↾ cres 5521   ∘ ccom 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-int 4839  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator