Theorem trclubgNEW 44199

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)

Hypothesis

Ref	Expression
trclubgNEW.rex	⊢ (𝜑 → 𝑅 ∈ V)

Assertion

Ref	Expression
trclubgNEW	⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))

Distinct variable group:   𝑥,𝑅

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem trclubgNEW

Step	Hyp	Ref	Expression
1		trclubgNEW.rex	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
2	1	dmexd 7884	. . . 4 ⊢ (𝜑 → dom 𝑅 ∈ V)
3		rnexg 7883	. . . . 5 ⊢ (𝑅 ∈ V → ran 𝑅 ∈ V)
4	1, 3	syl 17	. . . 4 ⊢ (𝜑 → ran 𝑅 ∈ V)
5	2, 4	xpexd 7734	. . 3 ⊢ (𝜑 → (dom 𝑅 × ran 𝑅) ∈ V)
6	1, 5	unexd 7737	. 2 ⊢ (𝜑 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V)
7		id 22	. . . 4 ⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → 𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
8	7, 7	coeq12d 5837	. . 3 ⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → (𝑥 ∘ 𝑥) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))))
9	8, 7	sseq12d 3970	. 2 ⊢ (𝑥 = (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → ((𝑥 ∘ 𝑥) ⊆ 𝑥 ↔ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))))
10		ssun1 4131	. . 3 ⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))
11	10	a1i 11	. 2 ⊢ (𝜑 → 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
12		cnvssrndm 6258	. . 3 ⊢ ◡𝑅 ⊆ (ran 𝑅 × dom 𝑅)
13		coundi 6234	. . . 4 ⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)))
14		cnvss 5845	. . . . . . . 8 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅))
15		coss2 5829	. . . . . . . 8 ⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)))
16	14, 15	syl 17	. . . . . . 7 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)))
17		cocnvcnv2 6246	. . . . . . 7 ⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡◡𝑅) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅)
18		cnvxp 6142	. . . . . . . 8 ⊢ ◡(ran 𝑅 × dom 𝑅) = (dom 𝑅 × ran 𝑅)
19	18	coeq2i 5833	. . . . . . 7 ⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ ◡(ran 𝑅 × dom 𝑅)) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))
20	16, 17, 19	3sstr3g 3989	. . . . . 6 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)))
21		ssequn1 4139	. . . . . 6 ⊢ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ⊆ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)))
22	20, 21	sylib 220	. . . . 5 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)))
23		coundir 6235	. . . . . 6 ⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) = ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
24		coss1 5828	. . . . . . . . . 10 ⊢ (◡◡𝑅 ⊆ ◡(ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
25	14, 24	syl 17	. . . . . . . . 9 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
26		cocnvcnv1 6245	. . . . . . . . 9 ⊢ (◡◡𝑅 ∘ (dom 𝑅 × ran 𝑅)) = (𝑅 ∘ (dom 𝑅 × ran 𝑅))
27	18	coeq1i 5832	. . . . . . . . 9 ⊢ (◡(ran 𝑅 × dom 𝑅) ∘ (dom 𝑅 × ran 𝑅)) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))
28	25, 26, 27	3sstr3g 3989	. . . . . . . 8 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
29		ssequn1 4139	. . . . . . . 8 ⊢ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
30	28, 29	sylib 220	. . . . . . 7 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)))
31		xptrrel 15003	. . . . . . . . 9 ⊢ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅)
32		ssun2 4132	. . . . . . . . 9 ⊢ (dom 𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))
33	31, 32	sstri 3946	. . . . . . . 8 ⊢ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))
34	33	a1i 11	. . . . . . 7 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
35	30, 34	eqsstrd 3971	. . . . . 6 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∘ (dom 𝑅 × ran 𝑅)) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
36	23, 35	eqsstrid 3975	. . . . 5 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
37	22, 36	eqsstrd 3971	. . . 4 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → (((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ 𝑅) ∪ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
38	13, 37	eqsstrid 3975	. . 3 ⊢ (◡𝑅 ⊆ (ran 𝑅 × dom 𝑅) → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
39	12, 38	mp1i 13	. 2 ⊢ (𝜑 → ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
40	6, 9, 11, 39	clublem 44191	1 ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  {cab 2741  Vcvv 3455   ∪ cun 3903   ⊆ wss 3905  ∩ cint 4906   × cxp 5646  ^◡ccnv 5647  dom cdm 5648  ran crn 5649   ∘ ccom 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-sep 5247  ax-pow 5323  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-br 5102  df-opab 5164  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660

This theorem is referenced by:  trclubNEW  44200