tfr2b

Description: Without assuming ax-rep , we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Hypothesis	tfr.1	$⊢ F = recs (G)$
	Assertion	tfr2b	$⊢ Ord A \to (A \in dom F \leftrightarrow {F ↾}_{A} \in V)$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$⊢ F = recs (G)$
2		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
3		eqid	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\}$
4	3	tfrlem15	$⊢ A \in On \to (A \in dom recs (G) \leftrightarrow {recs (G) ↾}_{A} \in V)$
5	1	dmeqi	$⊢ dom F = dom recs (G)$
6	5	eleq2i	$⊢ A \in dom F \leftrightarrow A \in dom recs (G)$
7	1	reseq1i	$⊢ {F ↾}_{A} = {recs (G) ↾}_{A}$
8	7	eleq1i	$⊢ {F ↾}_{A} \in V \leftrightarrow {recs (G) ↾}_{A} \in V$
9	4 6 8	3bitr4g	$⊢ A \in On \to (A \in dom F \leftrightarrow {F ↾}_{A} \in V)$
10		onprc	$⊢ \neg On \in V$
11		elex	$⊢ On \in dom F \to On \in V$
12	10 11	mto	$⊢ \neg On \in dom F$
13		eleq1	$⊢ A = On \to (A \in dom F \leftrightarrow On \in dom F)$
14	12 13	mtbiri	$⊢ A = On \to \neg A \in dom F$
15	3	tfrlem13	$⊢ \neg recs (G) \in V$
16	1 15	eqneltri	$⊢ \neg F \in V$
17		reseq2	$⊢ A = On \to {F ↾}_{A} = {F ↾}_{On}$
18	1	tfr1a	$⊢ (Fun F \land Lim dom F)$
19	18	simpli	$⊢ Fun F$
20		funrel	$⊢ Fun F \to Rel F$
21	19 20	ax-mp	$⊢ Rel F$
22	18	simpri	$⊢ Lim dom F$
23		limord	$⊢ Lim dom F \to Ord dom F$
24		ordsson	$⊢ Ord dom F \to dom F \subseteq On$
25	22 23 24	mp2b	$⊢ dom F \subseteq On$
26		relssres	$⊢ (Rel F \land dom F \subseteq On) \to {F ↾}_{On} = F$
27	21 25 26	mp2an	$⊢ {F ↾}_{On} = F$
28	17 27	eqtrdi	$⊢ A = On \to {F ↾}_{A} = F$
29	28	eleq1d	$⊢ A = On \to ({F ↾}_{A} \in V \leftrightarrow F \in V)$
30	16 29	mtbiri	$⊢ A = On \to \neg {F ↾}_{A} \in V$
31	14 30	2falsed	$⊢ A = On \to (A \in dom F \leftrightarrow {F ↾}_{A} \in V)$
32	9 31	jaoi	$⊢ (A \in On \lor A = On) \to (A \in dom F \leftrightarrow {F ↾}_{A} \in V)$
33	2 32	sylbi	$⊢ Ord A \to (A \in dom F \leftrightarrow {F ↾}_{A} \in V)$

Metamath Proof Explorer

Theorem tfr2b

Proof