dfac12lem3

	Ref	Expression
Hypotheses	dfac12.1	$⊢ φ \to A \in On$
	dfac12.3	$⊢ φ \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
	dfac12.4	$⊢ G = recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), F (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))))$
Assertion	dfac12lem3	$⊢ φ \to R_{1} (A) \in dom card$

Proof

Step	Hyp	Ref	Expression
1		dfac12.1	$⊢ φ \to A \in On$
2		dfac12.3	$⊢ φ \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
3		dfac12.4	$⊢ G = recs ((x \in V ⟼ (y \in R_{1} (dom x) ⟼ if (dom x = ⋃ dom x, (suc ⋃ ran ⋃ ran x \cdot_{𝑜} rank (y)) +_{𝑜} x (suc rank (y)) (y), F (({OrdIso (E, ran x (⋃ dom x))}^{-1} \circ x (⋃ dom x)) [y])))))$
4		fvex	$⊢ G (A) \in V$
5	4	rnex	$⊢ ran G (A) \in V$
6		ssid	$⊢ A \subseteq A$
7		sseq1	$⊢ m = n \to (m \subseteq A \leftrightarrow n \subseteq A)$
8		fveq2	$⊢ m = n \to G (m) = G (n)$
9		f1eq1	$⊢ G (m) = G (n) \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (n) : R_{1} (m) \underset{1-1}{⟶} On)$
10	8 9	syl	$⊢ m = n \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (n) : R_{1} (m) \underset{1-1}{⟶} On)$
11		fveq2	$⊢ m = n \to R_{1} (m) = R_{1} (n)$
12		f1eq2	$⊢ R_{1} (m) = R_{1} (n) \to (G (n) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
13	11 12	syl	$⊢ m = n \to (G (n) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
14	10 13	bitrd	$⊢ m = n \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
15	7 14	imbi12d	$⊢ m = n \to ((m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On) \leftrightarrow (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On))$
16	15	imbi2d	$⊢ m = n \to ((φ \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)) \leftrightarrow (φ \to (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On)))$
17		sseq1	$⊢ m = A \to (m \subseteq A \leftrightarrow A \subseteq A)$
18		fveq2	$⊢ m = A \to G (m) = G (A)$
19		f1eq1	$⊢ G (m) = G (A) \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (A) : R_{1} (m) \underset{1-1}{⟶} On)$
20	18 19	syl	$⊢ m = A \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (A) : R_{1} (m) \underset{1-1}{⟶} On)$
21		fveq2	$⊢ m = A \to R_{1} (m) = R_{1} (A)$
22		f1eq2	$⊢ R_{1} (m) = R_{1} (A) \to (G (A) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (A) : R_{1} (A) \underset{1-1}{⟶} On)$
23	21 22	syl	$⊢ m = A \to (G (A) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (A) : R_{1} (A) \underset{1-1}{⟶} On)$
24	20 23	bitrd	$⊢ m = A \to (G (m) : R_{1} (m) \underset{1-1}{⟶} On \leftrightarrow G (A) : R_{1} (A) \underset{1-1}{⟶} On)$
25	17 24	imbi12d	$⊢ m = A \to ((m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On) \leftrightarrow (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On))$
26	25	imbi2d	$⊢ m = A \to ((φ \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)) \leftrightarrow (φ \to (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On)))$
27		r19.21v	$⊢ \forall n \in m (φ \to (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On)) \leftrightarrow (φ \to \forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On))$
28		eloni	$⊢ m \in On \to Ord m$
29	28	ad2antrl	$⊢ (φ \land (m \in On \land m \subseteq A)) \to Ord m$
30		ordelss	$⊢ (Ord m \land n \in m) \to n \subseteq m$
31	29 30	sylan	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land n \in m) \to n \subseteq m$
32		simplrr	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land n \in m) \to m \subseteq A$
33	31 32	sstrd	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land n \in m) \to n \subseteq A$
34		pm5.5	$⊢ n \subseteq A \to ((n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \leftrightarrow G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
35	33 34	syl	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land n \in m) \to ((n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \leftrightarrow G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
36	35	ralbidva	$⊢ (φ \land (m \in On \land m \subseteq A)) \to (\forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \leftrightarrow \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On)$
37	1	ad2antrr	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to A \in On$
38	2	ad2antrr	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to F : 𝒫 har (R_{1} (A)) \underset{1-1}{⟶} On$
39		simplrl	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to m \in On$
40		eqid	$⊢ {OrdIso (E, ran G (⋃ m))}^{-1} \circ G (⋃ m) = {OrdIso (E, ran G (⋃ m))}^{-1} \circ G (⋃ m)$
41		simplrr	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to m \subseteq A$
42		fveq2	$⊢ n = z \to G (n) = G (z)$
43		f1eq1	$⊢ G (n) = G (z) \to (G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (n) \underset{1-1}{⟶} On)$
44	42 43	syl	$⊢ n = z \to (G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (n) \underset{1-1}{⟶} On)$
45		fveq2	$⊢ n = z \to R_{1} (n) = R_{1} (z)$
46		f1eq2	$⊢ R_{1} (n) = R_{1} (z) \to (G (z) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (z) \underset{1-1}{⟶} On)$
47	45 46	syl	$⊢ n = z \to (G (z) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (z) \underset{1-1}{⟶} On)$
48	44 47	bitrd	$⊢ n = z \to (G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (z) \underset{1-1}{⟶} On)$
49	48	cbvralvw	$⊢ \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow \forall z \in m G (z) : R_{1} (z) \underset{1-1}{⟶} On$
50	49	bilani	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to \forall z \in m G (z) : R_{1} (z) \underset{1-1}{⟶} On$
51	37 38 3 39 40 41 50	dfac12lem2	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to G (m) : R_{1} (m) \underset{1-1}{⟶} On$
52	51	ex	$⊢ (φ \land (m \in On \land m \subseteq A)) \to (\forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)$
53	36 52	sylbid	$⊢ (φ \land (m \in On \land m \subseteq A)) \to (\forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)$
54	53	expr	$⊢ (φ \land m \in On) \to (m \subseteq A \to (\forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to G (m) : R_{1} (m) \underset{1-1}{⟶} On))$
55	54	com23	$⊢ (φ \land m \in On) \to (\forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On))$
56	55	expcom	$⊢ m \in On \to (φ \to (\forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)))$
57	56	a2d	$⊢ m \in On \to ((φ \to \forall n \in m (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On)) \to (φ \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)))$
58	27 57	biimtrid	$⊢ m \in On \to (\forall n \in m (φ \to (n \subseteq A \to G (n) : R_{1} (n) \underset{1-1}{⟶} On)) \to (φ \to (m \subseteq A \to G (m) : R_{1} (m) \underset{1-1}{⟶} On)))$
59	16 26 58	tfis3	$⊢ A \in On \to (φ \to (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On))$
60	1 59	mpcom	$⊢ φ \to (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On)$
61	6 60	mpi	$⊢ φ \to G (A) : R_{1} (A) \underset{1-1}{⟶} On$
62		f1f	$⊢ G (A) : R_{1} (A) \underset{1-1}{⟶} On \to G (A) : R_{1} (A) ⟶ On$
63		frn	$⊢ G (A) : R_{1} (A) ⟶ On \to ran G (A) \subseteq On$
64	61 62 63	3syl	$⊢ φ \to ran G (A) \subseteq On$
65		onssnum	$⊢ (ran G (A) \in V \land ran G (A) \subseteq On) \to ran G (A) \in dom card$
66	5 64 65	sylancr	$⊢ φ \to ran G (A) \in dom card$
67		f1f1orn	$⊢ G (A) : R_{1} (A) \underset{1-1}{⟶} On \to G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A)$
68	61 67	syl	$⊢ φ \to G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A)$
69		fvex	$⊢ R_{1} (A) \in V$
70	69	f1oen	$⊢ G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A) \to R_{1} (A) \approx ran G (A)$
71		ennum	$⊢ R_{1} (A) \approx ran G (A) \to (R_{1} (A) \in dom card \leftrightarrow ran G (A) \in dom card)$
72	68 70 71	3syl	$⊢ φ \to (R_{1} (A) \in dom card \leftrightarrow ran G (A) \in dom card)$
73	66 72	mpbird	$⊢ φ \to R_{1} (A) \in dom card$

Metamath Proof Explorer

Theorem dfac12lem3

Proof