hartogslem1

	Ref	Expression
Hypotheses	hartogslem.2	$⊢ F = \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
	hartogslem.3	$⊢ R = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\}$
Assertion	hartogslem1	$⊢ (dom F \subseteq 𝒫 (A \times A) \land Fun F \land (A \in V \to ran F = \{x \in On \| x ≼ A\}))$

Proof

Step	Hyp	Ref	Expression
1		hartogslem.2	$⊢ F = \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
2		hartogslem.3	$⊢ R = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\}$
3	1	dmeqi	$⊢ dom F = dom \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
4		dmopab	$⊢ dom \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\} = \{r \| \exists y (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
5	3 4	eqtri	$⊢ dom F = \{r \| \exists y (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
6		simp3	$⊢ (dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \to r \subseteq dom r \times dom r$
7		simp1	$⊢ (dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \to dom r \subseteq A$
8		xpss12	$⊢ (dom r \subseteq A \land dom r \subseteq A) \to dom r \times dom r \subseteq A \times A$
9	7 7 8	syl2anc	$⊢ (dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \to dom r \times dom r \subseteq A \times A$
10	6 9	sstrd	$⊢ (dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \to r \subseteq A \times A$
11		velpw	$⊢ r \in 𝒫 (A \times A) \leftrightarrow r \subseteq A \times A$
12	10 11	sylibr	$⊢ (dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \to r \in 𝒫 (A \times A)$
13	12	ad2antrr	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to r \in 𝒫 (A \times A)$
14	13	exlimiv	$⊢ \exists y (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to r \in 𝒫 (A \times A)$
15	14	abssi	$⊢ \{r \| \exists y (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\} \subseteq 𝒫 (A \times A)$
16	5 15	eqsstri	$⊢ dom F \subseteq 𝒫 (A \times A)$
17		funopab4	$⊢ Fun \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
18	1	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
19	17 18	mpbir	$⊢ Fun F$
20	1	rneqi	$⊢ ran F = ran \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
21		rnopab	$⊢ ran \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\} = \{y \| \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
22	20 21	eqtri	$⊢ ran F = \{y \| \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
23		breq1	$⊢ x = y \to (x ≼ A \leftrightarrow y ≼ A)$
24	23	elrab	$⊢ y \in \{x \in On \| x ≼ A\} \leftrightarrow (y \in On \land y ≼ A)$
25		f1f	$⊢ f : y \underset{1-1}{⟶} A \to f : y ⟶ A$
26	25	adantl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to f : y ⟶ A$
27	26	frnd	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to ran f \subseteq A$
28		resss	$⊢ {I ↾}_{ran f} \subseteq I$
29		ssun2	$⊢ I \subseteq R \cup I$
30	28 29	sstri	$⊢ {I ↾}_{ran f} \subseteq R \cup I$
31		idssxp	$⊢ {I ↾}_{ran f} \subseteq ran f \times ran f$
32	30 31	ssini	$⊢ {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f)$
33	32	a1i	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f)$
34		inss2	$⊢ (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f$
35	34	a1i	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f$
36	27 33 35	3jca	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (ran f \subseteq A \land {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f) \land (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f)$
37		eloni	$⊢ y \in On \to Ord y$
38		ordwe	$⊢ Ord y \to E We y$
39	37 38	syl	$⊢ y \in On \to E We y$
40	39	adantr	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to E We y$
41		f1f1orn	$⊢ f : y \underset{1-1}{⟶} A \to f : y \underset{1-1 onto}{⟶} ran f$
42	41	adantl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to f : y \underset{1-1 onto}{⟶} ran f$
43		f1oiso	$⊢ (f : y \underset{1-1 onto}{⟶} ran f \land R = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = f (w) \land t = f (z)) \land w E z)\}) \to f {Isom}_{E, R} (y, ran f)$
44	42 2 43	sylancl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to f {Isom}_{E, R} (y, ran f)$
45		isores2	$⊢ f {Isom}_{E, R} (y, ran f) \leftrightarrow f {Isom}_{E, R \cap (ran f \times ran f)} (y, ran f)$
46	44 45	sylib	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to f {Isom}_{E, R \cap (ran f \times ran f)} (y, ran f)$
47		isowe	$⊢ f {Isom}_{E, R \cap (ran f \times ran f)} (y, ran f) \to (E We y \leftrightarrow (R \cap (ran f \times ran f)) We ran f)$
48	46 47	syl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (E We y \leftrightarrow (R \cap (ran f \times ran f)) We ran f)$
49	40 48	mpbid	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (R \cap (ran f \times ran f)) We ran f$
50		weso	$⊢ (R \cap (ran f \times ran f)) We ran f \to (R \cap (ran f \times ran f)) Or ran f$
51	49 50	syl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (R \cap (ran f \times ran f)) Or ran f$
52		inss2	$⊢ R \cap (ran f \times ran f) \subseteq ran f \times ran f$
53	52	brel	$⊢ x (R \cap (ran f \times ran f)) x \to (x \in ran f \land x \in ran f)$
54	53	simpld	$⊢ x (R \cap (ran f \times ran f)) x \to x \in ran f$
55		sonr	$⊢ ((R \cap (ran f \times ran f)) Or ran f \land x \in ran f) \to \neg x (R \cap (ran f \times ran f)) x$
56	51 54 55	syl2an	$⊢ ((y \in On \land f : y \underset{1-1}{⟶} A) \land x (R \cap (ran f \times ran f)) x) \to \neg x (R \cap (ran f \times ran f)) x$
57	56	pm2.01da	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to \neg x (R \cap (ran f \times ran f)) x$
58	57	alrimiv	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to \forall x \neg x (R \cap (ran f \times ran f)) x$
59		intirr	$⊢ (R \cap (ran f \times ran f)) \cap I = \emptyset \leftrightarrow \forall x \neg x (R \cap (ran f \times ran f)) x$
60	58 59	sylibr	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (R \cap (ran f \times ran f)) \cap I = \emptyset$
61		disj3	$⊢ (R \cap (ran f \times ran f)) \cap I = \emptyset \leftrightarrow R \cap (ran f \times ran f) = (R \cap (ran f \times ran f)) ∖ I$
62	60 61	sylib	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to R \cap (ran f \times ran f) = (R \cap (ran f \times ran f)) ∖ I$
63		weeq1	$⊢ R \cap (ran f \times ran f) = (R \cap (ran f \times ran f)) ∖ I \to ((R \cap (ran f \times ran f)) We ran f \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We ran f)$
64	62 63	syl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to ((R \cap (ran f \times ran f)) We ran f \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We ran f)$
65	49 64	mpbid	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to ((R \cap (ran f \times ran f)) ∖ I) We ran f$
66	37	adantr	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to Ord y$
67		isoeq3	$⊢ R \cap (ran f \times ran f) = (R \cap (ran f \times ran f)) ∖ I \to (f {Isom}_{E, R \cap (ran f \times ran f)} (y, ran f) \leftrightarrow f {Isom}_{E, (R \cap (ran f \times ran f)) ∖ I} (y, ran f))$
68	62 67	syl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (f {Isom}_{E, R \cap (ran f \times ran f)} (y, ran f) \leftrightarrow f {Isom}_{E, (R \cap (ran f \times ran f)) ∖ I} (y, ran f))$
69	46 68	mpbid	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to f {Isom}_{E, (R \cap (ran f \times ran f)) ∖ I} (y, ran f)$
70		vex	$⊢ f \in V$
71	70	rnex	$⊢ ran f \in V$
72		exse	$⊢ ran f \in V \to ((R \cap (ran f \times ran f)) ∖ I) Se ran f$
73	71 72	ax-mp	$⊢ ((R \cap (ran f \times ran f)) ∖ I) Se ran f$
74		eqid	$⊢ OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
75	74	oieu	$⊢ (((R \cap (ran f \times ran f)) ∖ I) We ran f \land ((R \cap (ran f \times ran f)) ∖ I) Se ran f) \to ((Ord y \land f {Isom}_{E, (R \cap (ran f \times ran f)) ∖ I} (y, ran f)) \leftrightarrow (y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f) \land f = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)))$
76	65 73 75	sylancl	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to ((Ord y \land f {Isom}_{E, (R \cap (ran f \times ran f)) ∖ I} (y, ran f)) \leftrightarrow (y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f) \land f = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)))$
77	66 69 76	mpbi2and	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to (y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f) \land f = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f))$
78	77	simpld	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
79	71 71	xpex	$⊢ ran f \times ran f \in V$
80	79	inex2	$⊢ (R \cup I) \cap (ran f \times ran f) \in V$
81		sseq1	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (r \subseteq ran f \times ran f \leftrightarrow (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f)$
82	34 81	mpbiri	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to r \subseteq ran f \times ran f$
83		dmss	$⊢ r \subseteq ran f \times ran f \to dom r \subseteq dom (ran f \times ran f)$
84	82 83	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom r \subseteq dom (ran f \times ran f)$
85		dmxpid	$⊢ dom (ran f \times ran f) = ran f$
86	84 85	sseqtrdi	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom r \subseteq ran f$
87		dmresi	$⊢ dom ({I ↾}_{ran f}) = ran f$
88		sseq2	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ({I ↾}_{ran f} \subseteq r \leftrightarrow {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f))$
89	32 88	mpbiri	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to {I ↾}_{ran f} \subseteq r$
90		dmss	$⊢ {I ↾}_{ran f} \subseteq r \to dom ({I ↾}_{ran f}) \subseteq dom r$
91	89 90	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom ({I ↾}_{ran f}) \subseteq dom r$
92	87 91	eqsstrrid	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ran f \subseteq dom r$
93	86 92	eqssd	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom r = ran f$
94	93	sseq1d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (dom r \subseteq A \leftrightarrow ran f \subseteq A)$
95	93	reseq2d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to {I ↾}_{dom r} = {I ↾}_{ran f}$
96		id	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to r = (R \cup I) \cap (ran f \times ran f)$
97	95 96	sseq12d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ({I ↾}_{dom r} \subseteq r \leftrightarrow {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f))$
98	93	sqxpeqd	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom r \times dom r = ran f \times ran f$
99	96 98	sseq12d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (r \subseteq dom r \times dom r \leftrightarrow (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f)$
100	94 97 99	3anbi123d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \leftrightarrow (ran f \subseteq A \land {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f) \land (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f))$
101		difeq1	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to r ∖ I = ((R \cup I) \cap (ran f \times ran f)) ∖ I$
102		difun2	$⊢ (R \cup I) ∖ I = R ∖ I$
103	102	ineq1i	$⊢ ((R \cup I) ∖ I) \cap (ran f \times ran f) = (R ∖ I) \cap (ran f \times ran f)$
104		indif1	$⊢ ((R \cup I) ∖ I) \cap (ran f \times ran f) = ((R \cup I) \cap (ran f \times ran f)) ∖ I$
105		indif1	$⊢ (R ∖ I) \cap (ran f \times ran f) = (R \cap (ran f \times ran f)) ∖ I$
106	103 104 105	3eqtr3i	$⊢ ((R \cup I) \cap (ran f \times ran f)) ∖ I = (R \cap (ran f \times ran f)) ∖ I$
107	101 106	eqtrdi	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to r ∖ I = (R \cap (ran f \times ran f)) ∖ I$
108		weeq1	$⊢ r ∖ I = (R \cap (ran f \times ran f)) ∖ I \to ((r ∖ I) We dom r \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We dom r)$
109	107 108	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ((r ∖ I) We dom r \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We dom r)$
110		weeq2	$⊢ dom r = ran f \to (((R \cap (ran f \times ran f)) ∖ I) We dom r \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We ran f)$
111	93 110	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (((R \cap (ran f \times ran f)) ∖ I) We dom r \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We ran f)$
112	109 111	bitrd	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ((r ∖ I) We dom r \leftrightarrow ((R \cap (ran f \times ran f)) ∖ I) We ran f)$
113	100 112	anbi12d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \leftrightarrow ((ran f \subseteq A \land {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f) \land (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f) \land ((R \cap (ran f \times ran f)) ∖ I) We ran f))$
114		oieq1	$⊢ r ∖ I = (R \cap (ran f \times ran f)) ∖ I \to OrdIso (r ∖ I, dom r) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, dom r)$
115	107 114	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to OrdIso (r ∖ I, dom r) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, dom r)$
116		oieq2	$⊢ dom r = ran f \to OrdIso ((R \cap (ran f \times ran f)) ∖ I, dom r) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
117	93 116	syl	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to OrdIso ((R \cap (ran f \times ran f)) ∖ I, dom r) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
118	115 117	eqtrd	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to OrdIso (r ∖ I, dom r) = OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
119	118	dmeqd	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to dom OrdIso (r ∖ I, dom r) = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)$
120	119	eqeq2d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to (y = dom OrdIso (r ∖ I, dom r) \leftrightarrow y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f))$
121	113 120	anbi12d	$⊢ r = (R \cup I) \cap (ran f \times ran f) \to ((((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \leftrightarrow (((ran f \subseteq A \land {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f) \land (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f) \land ((R \cap (ran f \times ran f)) ∖ I) We ran f) \land y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)))$
122	80 121	spcev	$⊢ (((ran f \subseteq A \land {I ↾}_{ran f} \subseteq (R \cup I) \cap (ran f \times ran f) \land (R \cup I) \cap (ran f \times ran f) \subseteq ran f \times ran f) \land ((R \cap (ran f \times ran f)) ∖ I) We ran f) \land y = dom OrdIso ((R \cap (ran f \times ran f)) ∖ I, ran f)) \to \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))$
123	36 65 78 122	syl21anc	$⊢ (y \in On \land f : y \underset{1-1}{⟶} A) \to \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))$
124	123	ex	$⊢ y \in On \to (f : y \underset{1-1}{⟶} A \to \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)))$
125	124	exlimdv	$⊢ y \in On \to (\exists f f : y \underset{1-1}{⟶} A \to \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)))$
126		brdomi	$⊢ y ≼ A \to \exists f f : y \underset{1-1}{⟶} A$
127	125 126	impel	$⊢ (y \in On \land y ≼ A) \to \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))$
128		simpr	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to y = dom OrdIso (r ∖ I, dom r)$
129		vex	$⊢ r \in V$
130	129	dmex	$⊢ dom r \in V$
131		eqid	$⊢ OrdIso (r ∖ I, dom r) = OrdIso (r ∖ I, dom r)$
132	131	oion	$⊢ dom r \in V \to dom OrdIso (r ∖ I, dom r) \in On$
133	130 132	ax-mp	$⊢ dom OrdIso (r ∖ I, dom r) \in On$
134	128 133	eqeltrdi	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to y \in On$
135	134	adantl	$⊢ (A \in V \land (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))) \to y \in On$
136		simplr	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to (r ∖ I) We dom r$
137	131	oien	$⊢ (dom r \in V \land (r ∖ I) We dom r) \to dom OrdIso (r ∖ I, dom r) \approx dom r$
138	130 136 137	sylancr	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to dom OrdIso (r ∖ I, dom r) \approx dom r$
139	128 138	eqbrtrd	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to y \approx dom r$
140		ssdomg	$⊢ A \in V \to (dom r \subseteq A \to dom r ≼ A)$
141		simpll1	$⊢ (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to dom r \subseteq A$
142	140 141	impel	$⊢ (A \in V \land (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))) \to dom r ≼ A$
143		endomtr	$⊢ (y \approx dom r \land dom r ≼ A) \to y ≼ A$
144	139 142 143	syl2an2	$⊢ (A \in V \land (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))) \to y ≼ A$
145	135 144	jca	$⊢ (A \in V \land (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))) \to (y \in On \land y ≼ A)$
146	145	ex	$⊢ A \in V \to ((((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to (y \in On \land y ≼ A))$
147	146	exlimdv	$⊢ A \in V \to (\exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)) \to (y \in On \land y ≼ A))$
148	127 147	impbid2	$⊢ A \in V \to ((y \in On \land y ≼ A) \leftrightarrow \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)))$
149	24 148	syl5bb	$⊢ A \in V \to (y \in \{x \in On \| x ≼ A\} \leftrightarrow \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r)))$
150	149	abbi2dv	$⊢ A \in V \to \{x \in On \| x ≼ A\} = \{y \| \exists r (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
151	22 150	eqtr4id	$⊢ A \in V \to ran F = \{x \in On \| x ≼ A\}$
152	16 19 151	3pm3.2i	$⊢ (dom F \subseteq 𝒫 (A \times A) \land Fun F \land (A \in V \to ran F = \{x \in On \| x ≼ A\}))$

Metamath Proof Explorer

Theorem hartogslem1

Proof