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

Theorem rtrclex 36943
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 3738 . . . 4 𝐴 ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2 coundir 5554 . . . . . . 7 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
3 coundi 5553 . . . . . . . . 9 (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
4 cossxp 5575 . . . . . . . . . . 11 (𝐴𝐴) ⊆ (dom 𝐴 × ran 𝐴)
5 ssun1 3738 . . . . . . . . . . . 12 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
6 ssun2 3739 . . . . . . . . . . . 12 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
7 xpss12 5148 . . . . . . . . . . . 12 ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
85, 6, 7mp2an 704 . . . . . . . . . . 11 (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
94, 8sstri 3577 . . . . . . . . . 10 (𝐴𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
10 cossxp 5575 . . . . . . . . . . 11 (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴)
11 dmxpss 5484 . . . . . . . . . . . 12 dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
12 xpss12 5148 . . . . . . . . . . . 12 ((dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
1311, 6, 12mp2an 704 . . . . . . . . . . 11 (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
1410, 13sstri 3577 . . . . . . . . . 10 (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
159, 14unssi 3750 . . . . . . . . 9 ((𝐴𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
163, 15eqsstri 3598 . . . . . . . 8 (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
17 coundi 5553 . . . . . . . . 9 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
18 cossxp 5575 . . . . . . . . . . 11 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
19 rnxpss 5485 . . . . . . . . . . . 12 ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
20 xpss12 5148 . . . . . . . . . . . 12 ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
215, 19, 20mp2an 704 . . . . . . . . . . 11 (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2218, 21sstri 3577 . . . . . . . . . 10 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
23 xpidtr 5437 . . . . . . . . . 10 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2422, 23unssi 3750 . . . . . . . . 9 ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2517, 24eqsstri 3598 . . . . . . . 8 (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
2616, 25unssi 3750 . . . . . . 7 ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
272, 26eqsstri 3598 . . . . . 6 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
28 ssun2 3739 . . . . . 6 ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2927, 28sstri 3577 . . . . 5 ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
30 dmun 5253 . . . . . . . . . . 11 dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
31 dmxpid 5266 . . . . . . . . . . . . 13 dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3231uneq2i 3726 . . . . . . . . . . . 12 (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
33 ssequn1 3745 . . . . . . . . . . . . 13 (dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
345, 33mpbi 219 . . . . . . . . . . . 12 (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3532, 34eqtri 2632 . . . . . . . . . . 11 (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
3630, 35eqtri 2632 . . . . . . . . . 10 dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
37 rnun 5460 . . . . . . . . . . 11 ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
38 rnxpid 5486 . . . . . . . . . . . . 13 ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
3938uneq2i 3726 . . . . . . . . . . . 12 (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
40 ssequn1 3745 . . . . . . . . . . . . 13 (ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
416, 40mpbi 219 . . . . . . . . . . . 12 (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
4239, 41eqtri 2632 . . . . . . . . . . 11 (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
4337, 42eqtri 2632 . . . . . . . . . 10 ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
4436, 43uneq12i 3727 . . . . . . . . 9 (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴))
45 unidm 3718 . . . . . . . . 9 ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
4644, 45eqtri 2632 . . . . . . . 8 (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = (dom 𝐴 ∪ ran 𝐴)
4746reseq2i 5314 . . . . . . 7 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) = ( I ↾ (dom 𝐴 ∪ ran 𝐴))
48 fnresi 5922 . . . . . . . . 9 ( I ↾ (dom 𝐴 ∪ ran 𝐴)) Fn (dom 𝐴 ∪ ran 𝐴)
49 fnrel 5903 . . . . . . . . 9 (( I ↾ (dom 𝐴 ∪ ran 𝐴)) Fn (dom 𝐴 ∪ ran 𝐴) → Rel ( I ↾ (dom 𝐴 ∪ ran 𝐴)))
50 relssdmrn 5573 . . . . . . . . 9 (Rel ( I ↾ (dom 𝐴 ∪ ran 𝐴)) → ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom ( I ↾ (dom 𝐴 ∪ ran 𝐴)) × ran ( I ↾ (dom 𝐴 ∪ ran 𝐴))))
5148, 49, 50mp2b 10 . . . . . . . 8 ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom ( I ↾ (dom 𝐴 ∪ ran 𝐴)) × ran ( I ↾ (dom 𝐴 ∪ ran 𝐴)))
52 dmresi 5376 . . . . . . . . 9 dom ( I ↾ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
53 rnresi 5398 . . . . . . . . 9 ran ( I ↾ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
5452, 53xpeq12i 5061 . . . . . . . 8 (dom ( I ↾ (dom 𝐴 ∪ ran 𝐴)) × ran ( I ↾ (dom 𝐴 ∪ ran 𝐴))) = ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
5551, 54sseqtri 3600 . . . . . . 7 ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
5647, 55eqsstri 3598 . . . . . 6 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
5756, 28sstri 3577 . . . . 5 ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
5829, 57pm3.2i 470 . . . 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 𝐴))))
59 rtrclexlem 36942 . . . . 5 (𝐴 ∈ V → (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∈ V)
60 id 22 . . . . . . . . . . 11 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → 𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
6160, 60coeq12d 5208 . . . . . . . . . 10 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (𝑥𝑥) = ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
6261, 60sseq12d 3597 . . . . . . . . 9 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
63 dmeq 5246 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → dom 𝑥 = dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
64 rneq 5272 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ran 𝑥 = ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
6563, 64uneq12d 3730 . . . . . . . . . . 11 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
6665reseq2d 5317 . . . . . . . . . 10 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))))
6766, 60sseq12d 3597 . . . . . . . . 9 (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
6862, 67anbi12d 743 . . . . . . . 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 𝐴))))))
6968cleq2lem 36933 . . . . . . 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 𝐴)))))))
7069biimprd 237 . . . . . 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 𝑥)) ⊆ 𝑥))))
7170adantl 481 . . . . 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 𝑥)) ⊆ 𝑥))))
7259, 71spcimedv 3265 . . . 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 𝑥)) ⊆ 𝑥))))
731, 58, 72mp2ani 710 . . 3 (𝐴 ∈ V → ∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
74 exsimpl 1783 . . . 4 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → ∃𝑥 𝐴𝑥)
75 vex 3176 . . . . . 6 𝑥 ∈ V
7675ssex 4730 . . . . 5 (𝐴𝑥𝐴 ∈ V)
7776exlimiv 1845 . . . 4 (∃𝑥 𝐴𝑥𝐴 ∈ V)
7874, 77syl 17 . . 3 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → 𝐴 ∈ V)
7973, 78impbii 198 . 2 (𝐴 ∈ V ↔ ∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
80 intexab 4749 . 2 (∃𝑥(𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) ↔ {𝑥 ∣ (𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
8179, 80bitri 263 1 (𝐴 ∈ V ↔ {𝑥 ∣ (𝐴𝑥 ∧ ((𝑥𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wex 1695  wcel 1977  {cab 2596  Vcvv 3173  cun 3538  wss 3540   cint 4410   I cid 4948   × cxp 5036  dom cdm 5038  ran crn 5039  cres 5040  ccom 5042  Rel wrel 5043   Fn wfn 5799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-int 4411  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-fun 5806  df-fn 5807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator