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 44714

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 4176	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
2		coundir 6249	. . . . 5 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
3		coundi 6248	. . . . . . 7 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
4		cossxp 6274	. . . . . . . . 9 ⊢ (𝐴 ∘ 𝐴) ⊆ (dom 𝐴 × ran 𝐴)
5		ssun1 4176	. . . . . . . . . 10 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
6		ssun2 4177	. . . . . . . . . 10 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
7		xpss12 5665	. . . . . . . . . 10 ⊢ ((dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) ∧ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)) → (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
8	5, 6, 7	mp2an 705	. . . . . . . . 9 ⊢ (dom 𝐴 × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
9	4, 8	sstri 3917	. . . . . . . 8 ⊢ (𝐴 ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
10		cossxp 6274	. . . . . . . . 9 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴)
11		dmxpss 6162	. . . . . . . . . 10 ⊢ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
12		xpss12 5665	. . . . . . . . . 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 705	. . . . . . . . 9 ⊢ (dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) × ran 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
14	10, 13	sstri 3917	. . . . . . . 8 ⊢ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
15	9, 14	unssi 4189	. . . . . . 7 ⊢ ((𝐴 ∘ 𝐴) ∪ (𝐴 ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
16	3, 15	eqsstri 3954	. . . . . 6 ⊢ (𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
17		coundi 6248	. . . . . . 7 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) = ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
18		cossxp 6274	. . . . . . . . 9 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
19		rnxpss 6163	. . . . . . . . . 10 ⊢ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (dom 𝐴 ∪ ran 𝐴)
20		xpss12 5665	. . . . . . . . . 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 705	. . . . . . . . 9 ⊢ (dom 𝐴 × ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
22	18, 21	sstri 3917	. . . . . . . 8 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
23		xpidtr 6115	. . . . . . . 8 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
24	22, 23	unssi 4189	. . . . . . 7 ⊢ ((((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ 𝐴) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
25	17, 24	eqsstri 3954	. . . . . 6 ⊢ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
26	16, 25	unssi 4189	. . . . 5 ⊢ ((𝐴 ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ∪ (((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
27	2, 26	eqsstri 3954	. . . 4 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
28		ssun2 4177	. . . 4 ⊢ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
29	27, 28	sstri 3917	. . 3 ⊢ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
30		dmun 5891	. . . . . . . 8 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
31	5, 11	unssi 4189	. . . . . . . 8 ⊢ (dom 𝐴 ∪ dom ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
32	30, 31	eqsstri 3954	. . . . . . 7 ⊢ dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
33		rnun 6135	. . . . . . . 8 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) = (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
34	6, 19	unssi 4189	. . . . . . . 8 ⊢ (ran 𝐴 ∪ ran ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
35	33, 34	eqsstri 3954	. . . . . . 7 ⊢ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ⊆ (dom 𝐴 ∪ ran 𝐴)
36	32, 35	unssi 4189	. . . . . 6 ⊢ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (dom 𝐴 ∪ ran 𝐴)
37		ssres2 5994	. . . . . 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 6040	. . . . 5 ⊢ ( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
40	38, 39	sstri 3917	. . . 4 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))
41	40, 28	sstri 3917	. . 3 ⊢ ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))
42		id 23	. . 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 705	. 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 3472	. . . . 5 ⊢ 𝐴 ∈ V
46	45	dmex 7921	. . . . . . 7 ⊢ dom 𝐴 ∈ V
47	45	rnex 7922	. . . . . . 7 ⊢ ran 𝐴 ∈ V
48	46, 47	unex 7761	. . . . . 6 ⊢ (dom 𝐴 ∪ ran 𝐴) ∈ V
49	48, 48	xpex 7767	. . . . 5 ⊢ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)) ∈ V
50	45, 49	unex 7761	. . . 4 ⊢ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∈ V
51		id 23	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → 𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
52	51, 51	coeq12d 5841	. . . . . . 7 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (𝑥 ∘ 𝑥) = ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
53	52, 51	sseq12d 3941	. . . . . 6 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∘ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))) ⊆ (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
54		dmeq 5884	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → dom 𝑥 = dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
55		rneq 5917	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ran 𝑥 = ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))
56	54, 55	uneq12d 4168	. . . . . . . 8 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴)))))
57	56	reseq2d 5969	. . . . . . 7 ⊢ (𝑥 = (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))) ∪ ran (𝐴 ∪ ((dom 𝐴 ∪ ran 𝐴) × (dom 𝐴 ∪ ran 𝐴))))))
58	57, 51	sseq12d 3941	. . . . . 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 644	. . . . 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 44701	. . . 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 3560	. . 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 5306	. . 3 ⊢ (∃𝑥(𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
63	61, 62	sylib 221	. 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 705	1 ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1569 ∃wex 1811 ∈ wcel 2144 {cab 2738 Vcvv 3450 ⊆ wss 3895 ∪ cun 4149 ∩ cint 4906 I cid 5544 × cxp 5648 dom cdm 5650 ran crn 5651 ↾ cres 5652 ∘ ccom 5654

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-br 5103 df-opab 5167 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662

This theorem is used by: dfrtrcl5 44722

W3C validator