rtrclexi - Mathbox for Richard Penner

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

Theorem rtrclexi 41118

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

**Hypothesis**
Ref	Expression
rtrclexi.1	⊢ 𝐴 ∈ 𝑉

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

Distinct variable group: 𝑥,𝐴 Allowed substitution hint: 𝑉(𝑥)

**Proof of Theorem rtrclexi**
Step	Hyp	Ref	Expression
1		ssun1 4102	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2		coundir 6141	. . . . 5 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
3		coundi 6140	. . . . . . 7 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
4		cossxp 6164	. . . . . . . . 9 ⊢ (𝐴 ∘ 𝐴) ⊆ (dom 𝐴 × ran 𝐴)
5		ssun1 4102	. . . . . . . . . 10 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
6		ssun2 4103	. . . . . . . . . 10 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
7		xpss12 5595	. . . . . . . . . 10 ⊢ ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
8	5, 6, 7	mp2an 688	. . . . . . . . 9 ⊢ (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
9	4, 8	sstri 3926	. . . . . . . 8 ⊢ (𝐴 ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
10		cossxp 6164	. . . . . . . . 9 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴)
11		dmxpss 6063	. . . . . . . . . 10 ⊢ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
12		xpss12 5595	. . . . . . . . . 10 ⊢ ((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 688	. . . . . . . . 9 ⊢ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
14	10, 13	sstri 3926	. . . . . . . 8 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
15	9, 14	unssi 4115	. . . . . . 7 ⊢ ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
16	3, 15	eqsstri 3951	. . . . . 6 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
17		coundi 6140	. . . . . . 7 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
18		cossxp 6164	. . . . . . . . 9 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
19		rnxpss 6064	. . . . . . . . . 10 ⊢ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
20		xpss12 5595	. . . . . . . . . 10 ⊢ ((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 688	. . . . . . . . 9 ⊢ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
22	18, 21	sstri 3926	. . . . . . . 8 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
23		xpidtr 6016	. . . . . . . 8 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
24	22, 23	unssi 4115	. . . . . . 7 ⊢ ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
25	17, 24	eqsstri 3951	. . . . . 6 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
26	16, 25	unssi 4115	. . . . 5 ⊢ ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
27	2, 26	eqsstri 3951	. . . 4 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
28		ssun2 4103	. . . 4 ⊢ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
29	27, 28	sstri 3926	. . 3 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
30		dmun 5808	. . . . . . . 8 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
31	5, 11	unssi 4115	. . . . . . . 8 ⊢ (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
32	30, 31	eqsstri 3951	. . . . . . 7 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
33		rnun 6038	. . . . . . . 8 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
34	6, 19	unssi 4115	. . . . . . . 8 ⊢ (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
35	33, 34	eqsstri 3951	. . . . . . 7 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
36	32, 35	unssi 4115	. . . . . 6 ⊢ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (dom 𝐴 ∪ ran 𝐴)
37		ssres2 5908	. . . . . 6 ⊢ ((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 𝐴)))
38	36, 37	ax-mp 5	. . . . 5 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ( I ↾ (dom 𝐴 ∪ ran 𝐴))
39		idssxp 5945	. . . . 5 ⊢ ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
40	38, 39	sstri 3926	. . . 4 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
41	40, 28	sstri 3926	. . 3 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
42		id 22	. . 3 ⊢ ((((𝐴 ∪ ((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 𝐴)))))
43	29, 41, 42	mp2an 688	. 2 ⊢ (((𝐴 ∪ ((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		rtrclexi.1	. . . . . 6 ⊢ 𝐴 ∈ 𝑉
45	44	elexi 3441	. . . . 5 ⊢ 𝐴 ∈ V
46	45	dmex 7732	. . . . . . 7 ⊢ dom 𝐴 ∈ V
47	45	rnex 7733	. . . . . . 7 ⊢ ran 𝐴 ∈ V
48	46, 47	unex 7574	. . . . . 6 ⊢ (dom 𝐴 ∪ ran 𝐴) ∈ V
49	48, 48	xpex 7581	. . . . 5 ⊢ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∈ V
50	45, 49	unex 7574	. . . 4 ⊢ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∈ V
51		id 22	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → 𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
52	51, 51	coeq12d 5762	. . . . . . 7 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (𝑥 ∘ 𝑥) = ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
53	52, 51	sseq12d 3950	. . . . . 6 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
54		dmeq 5801	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → dom 𝑥 = dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
55		rneq 5834	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ran 𝑥 = ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
56	54, 55	uneq12d 4094	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
57	56	reseq2d 5880	. . . . . . 7 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))))
58	57, 51	sseq12d 3950	. . . . . 6 ⊢ (𝑥 = (𝐴 ∪ ((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 630	. . . . 5 ⊢ (𝑥 = (𝐴 ∪ ((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 41105	. . . 4 ⊢ (𝑥 = (𝐴 ∪ ((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 3535	. . 3 ⊢ ((𝐴 ⊆ (𝐴 ∪ ((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 5258	. . 3 ⊢ (∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
63	61, 62	sylib 217	. 2 ⊢ ((𝐴 ⊆ (𝐴 ∪ ((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	1, 43, 63	mp2an 688	1 ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 = wceq 1539 ∃wex 1783 ∈ wcel 2108 {cab 2715 Vcvv 3422 ∪ cun 3881 ⊆ wss 3883 ∩ cint 4876 I cid 5479 × cxp 5578 dom cdm 5580 ran crn 5581 ↾ cres 5582 ∘ ccom 5584

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-int 4877 df-br 5071 df-opab 5133 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592

This theorem is referenced by: dfrtrcl5 41126

W3C validator