Theorem rtrclex 43970

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

Step	Hyp	Ref	Expression
1		ssun1 4132	. . . 4 ⊢ 𝐴 ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2		coundir 6214	. . . . . . 7 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
3		coundi 6213	. . . . . . . . 9 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
4		cossxp 6238	. . . . . . . . . . 11 ⊢ (𝐴 ∘ 𝐴) ⊆ (dom 𝐴 × ran 𝐴)
5		ssun1 4132	. . . . . . . . . . . 12 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
6		ssun2 4133	. . . . . . . . . . . 12 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
7		xpss12 5647	. . . . . . . . . . . 12 ⊢ ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
8	5, 6, 7	mp2an 693	. . . . . . . . . . 11 ⊢ (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
9	4, 8	sstri 3945	. . . . . . . . . 10 ⊢ (𝐴 ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
10		cossxp 6238	. . . . . . . . . . 11 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴)
11		dmxpss 6137	. . . . . . . . . . . 12 ⊢ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
12		xpss12 5647	. . . . . . . . . . . 12 ⊢ ((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 693	. . . . . . . . . . 11 ⊢ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
14	10, 13	sstri 3945	. . . . . . . . . 10 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
15	9, 14	unssi 4145	. . . . . . . . 9 ⊢ ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
16	3, 15	eqsstri 3982	. . . . . . . 8 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
17		coundi 6213	. . . . . . . . 9 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
18		cossxp 6238	. . . . . . . . . . 11 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
19		rnxpss 6138	. . . . . . . . . . . 12 ⊢ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
20		xpss12 5647	. . . . . . . . . . . 12 ⊢ ((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 693	. . . . . . . . . . 11 ⊢ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
22	18, 21	sstri 3945	. . . . . . . . . 10 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
23		xpidtr 6087	. . . . . . . . . 10 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
24	22, 23	unssi 4145	. . . . . . . . 9 ⊢ ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
25	17, 24	eqsstri 3982	. . . . . . . 8 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
26	16, 25	unssi 4145	. . . . . . 7 ⊢ ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
27	2, 26	eqsstri 3982	. . . . . 6 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
28		ssun2 4133	. . . . . 6 ⊢ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
29	27, 28	sstri 3945	. . . . 5 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
30		dmun 5867	. . . . . . . . . . 11 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
31		dmxpid 5887	. . . . . . . . . . . 12 ⊢ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
32	31	uneq2i 4119	. . . . . . . . . . 11 ⊢ (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
33		ssequn1 4140	. . . . . . . . . . . 12 ⊢ (dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
34	5, 33	mpbi 230	. . . . . . . . . . 11 ⊢ (dom 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
35	30, 32, 34	3eqtri 2764	. . . . . . . . . 10 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
36		rnun 6111	. . . . . . . . . . 11 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
37		rnxpid 6139	. . . . . . . . . . . 12 ⊢ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
38	37	uneq2i 4119	. . . . . . . . . . 11 ⊢ (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴))
39		ssequn1 4140	. . . . . . . . . . . 12 ⊢ (ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ↔ (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴))
40	6, 39	mpbi 230	. . . . . . . . . . 11 ⊢ (ran 𝐴 ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
41	36, 38, 40	3eqtri 2764	. . . . . . . . . 10 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ ran 𝐴)
42	35, 41	uneq12i 4120	. . . . . . . . 9 ⊢ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴))
43		unidm 4111	. . . . . . . . 9 ⊢ ((dom 𝐴 ∪ ran 𝐴) ∪ (dom 𝐴 ∪ ran 𝐴)) = (dom 𝐴 ∪ ran 𝐴)
44	42, 43	eqtri 2760	. . . . . . . 8 ⊢ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = (dom 𝐴 ∪ ran 𝐴)
45	44	reseq2i 5943	. . . . . . 7 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) = ( I ↾ (dom 𝐴 ∪ ran 𝐴))
46		idssxp 6016	. . . . . . 7 ⊢ ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
47	45, 46	eqsstri 3982	. . . . . 6 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
48	47, 28	sstri 3945	. . . . 5 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
49	29, 48	pm3.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 𝐴))))
50		rtrclexlem 43969	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∈ V)
51		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → 𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
52	51, 51	coeq12d 5821	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (𝑥 ∘ 𝑥) = ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
53	52, 51	sseq12d 3969	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
54		dmeq 5860	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → dom 𝑥 = dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
55		rneq 5893	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ran 𝑥 = ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
56	54, 55	uneq12d 4123	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
57	56	reseq2d 5946	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))))
58	57, 51	sseq12d 3969	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((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 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 𝐴))))))
60	59	cleq2lem 43961	. . . . . . 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 𝐴)))))))
61	60	biimprd 248	. . . . . 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 𝑥)) ⊆ 𝑥))))
62	61	adantl 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 𝑥)) ⊆ 𝑥))))
63	50, 62	spcimedv 3551	. . . 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 𝑥)) ⊆ 𝑥))))
64	1, 49, 63	mp2ani 699	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
65		exsimpl 1870	. . . 4 ⊢ (∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → ∃𝑥 𝐴 ⊆ 𝑥)
66		vex 3446	. . . . . 6 ⊢ 𝑥 ∈ V
67	66	ssex 5268	. . . . 5 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
68	67	exlimiv 1932	. . . 4 ⊢ (∃𝑥 𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
69	65, 68	syl 17	. . 3 ⊢ (∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) → 𝐴 ∈ V)
70	64, 69	impbii 209	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)))
71		intexab 5293	. 2 ⊢ (∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
72	70, 71	bitri 275	1 ⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  ∩ cint 4904   I cid 5526   × cxp 5630  dom cdm 5632  ran crn 5633   ↾ cres 5634   ∘ ccom 5636

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644

This theorem is referenced by: (None)