rnttrcl

Description: The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024)

		Ref	Expression
	Assertion	rnttrcl	$⊢ ran t++ R = ran R$

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	$⊢ t++ R = \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
2	1	rneqi	$⊢ ran t++ R = ran \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
3		rnopab	$⊢ ran \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\} = \{y \| \exists x \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
4	2 3	eqtri	$⊢ ran t++ R = \{y \| \exists x \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\}$
5		fveq2	$⊢ a = ⋃ n \to f (a) = f (⋃ n)$
6		suceq	$⊢ a = ⋃ n \to suc a = suc ⋃ n$
7	6	fveq2d	$⊢ a = ⋃ n \to f (suc a) = f (suc ⋃ n)$
8	5 7	breq12d	$⊢ a = ⋃ n \to (f (a) R f (suc a) \leftrightarrow f (⋃ n) R f (suc ⋃ n))$
9		simpr3	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to \forall a \in n f (a) R f (suc a)$
10		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
11	10	difeq2i	$⊢ ω ∖ 1_{𝑜} = ω ∖ suc \emptyset$
12	11	eleq2i	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow n \in (ω ∖ suc \emptyset)$
13		peano1	$⊢ \emptyset \in ω$
14		eldifsucnn	$⊢ \emptyset \in ω \to (n \in (ω ∖ suc \emptyset) \leftrightarrow \exists x \in (ω ∖ \emptyset) n = suc x)$
15	13 14	ax-mp	$⊢ n \in (ω ∖ suc \emptyset) \leftrightarrow \exists x \in (ω ∖ \emptyset) n = suc x$
16		dif0	$⊢ ω ∖ \emptyset = ω$
17	16	rexeqi	$⊢ \exists x \in (ω ∖ \emptyset) n = suc x \leftrightarrow \exists x \in ω n = suc x$
18	12 15 17	3bitri	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow \exists x \in ω n = suc x$
19		nnord	$⊢ x \in ω \to Ord x$
20		ordunisuc	$⊢ Ord x \to ⋃ suc x = x$
21	19 20	syl	$⊢ x \in ω \to ⋃ suc x = x$
22		vex	$⊢ x \in V$
23	22	sucid	$⊢ x \in suc x$
24	21 23	eqeltrdi	$⊢ x \in ω \to ⋃ suc x \in suc x$
25		unieq	$⊢ n = suc x \to ⋃ n = ⋃ suc x$
26		id	$⊢ n = suc x \to n = suc x$
27	25 26	eleq12d	$⊢ n = suc x \to (⋃ n \in n \leftrightarrow ⋃ suc x \in suc x)$
28	24 27	syl5ibrcom	$⊢ x \in ω \to (n = suc x \to ⋃ n \in n)$
29	28	rexlimiv	$⊢ \exists x \in ω n = suc x \to ⋃ n \in n$
30	18 29	sylbi	$⊢ n \in (ω ∖ 1_{𝑜}) \to ⋃ n \in n$
31	30	adantr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to ⋃ n \in n$
32	8 9 31	rspcdva	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (⋃ n) R f (suc ⋃ n)$
33		suceq	$⊢ ⋃ suc x = x \to suc ⋃ suc x = suc x$
34	21 33	syl	$⊢ x \in ω \to suc ⋃ suc x = suc x$
35		suceq	$⊢ ⋃ n = ⋃ suc x \to suc ⋃ n = suc ⋃ suc x$
36	25 35	syl	$⊢ n = suc x \to suc ⋃ n = suc ⋃ suc x$
37	36 26	eqeq12d	$⊢ n = suc x \to (suc ⋃ n = n \leftrightarrow suc ⋃ suc x = suc x)$
38	34 37	syl5ibrcom	$⊢ x \in ω \to (n = suc x \to suc ⋃ n = n)$
39	38	rexlimiv	$⊢ \exists x \in ω n = suc x \to suc ⋃ n = n$
40	18 39	sylbi	$⊢ n \in (ω ∖ 1_{𝑜}) \to suc ⋃ n = n$
41	40	fveq2d	$⊢ n \in (ω ∖ 1_{𝑜}) \to f (suc ⋃ n) = f (n)$
42	41	adantr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (suc ⋃ n) = f (n)$
43		simpr2r	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (n) = y$
44	42 43	eqtrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (suc ⋃ n) = y$
45	32 44	breqtrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to f (⋃ n) R y$
46		fvex	$⊢ f (⋃ n) \in V$
47		vex	$⊢ y \in V$
48	46 47	brelrn	$⊢ f (⋃ n) R y \to y \in ran R$
49	45 48	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))) \to y \in ran R$
50	49	ex	$⊢ n \in (ω ∖ 1_{𝑜}) \to ((f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to y \in ran R)$
51	50	exlimdv	$⊢ n \in (ω ∖ 1_{𝑜}) \to (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to y \in ran R)$
52	51	rexlimiv	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to y \in ran R$
53	52	exlimiv	$⊢ \exists x \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a)) \to y \in ran R$
54	53	abssi	$⊢ \{y \| \exists x \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall a \in n f (a) R f (suc a))\} \subseteq ran R$
55	4 54	eqsstri	$⊢ ran t++ R \subseteq ran R$
56		rnresv	$⊢ ran ({R ↾}_{V}) = ran R$
57		relres	$⊢ Rel ({R ↾}_{V})$
58		ssttrcl	$⊢ Rel ({R ↾}_{V}) \to {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
59	57 58	ax-mp	$⊢ {R ↾}_{V} \subseteq t++ ({R ↾}_{V})$
60		ttrclresv	$⊢ t++ ({R ↾}_{V}) = t++ R$
61	59 60	sseqtri	$⊢ {R ↾}_{V} \subseteq t++ R$
62	61	rnssi	$⊢ ran ({R ↾}_{V}) \subseteq ran t++ R$
63	56 62	eqsstrri	$⊢ ran R \subseteq ran t++ R$
64	55 63	eqssi	$⊢ ran t++ R = ran R$

Metamath Proof Explorer

Theorem rnttrcl

Proof