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		simpr	$⊢ ((φ \land (m \in On \land m \subseteq A)) \land \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On) \to \forall n \in m G (n) : R_{1} (n) \underset{1-1}{⟶} On$
43		fveq2	$⊢ n = z \to G (n) = G (z)$
44		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)$
45	43 44	syl	$⊢ n = z \to (G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (n) \underset{1-1}{⟶} On)$
46		fveq2	$⊢ n = z \to R_{1} (n) = R_{1} (z)$
47		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)$
48	46 47	syl	$⊢ n = z \to (G (z) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (z) \underset{1-1}{⟶} On)$
49	45 48	bitrd	$⊢ n = z \to (G (n) : R_{1} (n) \underset{1-1}{⟶} On \leftrightarrow G (z) : R_{1} (z) \underset{1-1}{⟶} On)$
50	49	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$
51	42 50	sylib	$⊢ ((φ \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$
52	37 38 3 39 40 41 51	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$
53	52	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)$
54	36 53	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)$
55	54	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))$
56	55	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))$
57	56	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)))$
58	57	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)))$
59	27 58	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)))$
60	16 26 59	tfis3	$⊢ A \in On \to (φ \to (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On))$
61	1 60	mpcom	$⊢ φ \to (A \subseteq A \to G (A) : R_{1} (A) \underset{1-1}{⟶} On)$
62	6 61	mpi	$⊢ φ \to G (A) : R_{1} (A) \underset{1-1}{⟶} On$
63		f1f	$⊢ G (A) : R_{1} (A) \underset{1-1}{⟶} On \to G (A) : R_{1} (A) ⟶ On$
64		frn	$⊢ G (A) : R_{1} (A) ⟶ On \to ran G (A) \subseteq On$
65	62 63 64	3syl	$⊢ φ \to ran G (A) \subseteq On$
66		onssnum	$⊢ (ran G (A) \in V \land ran G (A) \subseteq On) \to ran G (A) \in dom card$
67	5 65 66	sylancr	$⊢ φ \to ran G (A) \in dom card$
68		f1f1orn	$⊢ G (A) : R_{1} (A) \underset{1-1}{⟶} On \to G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A)$
69	62 68	syl	$⊢ φ \to G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A)$
70		fvex	$⊢ R_{1} (A) \in V$
71	70	f1oen	$⊢ G (A) : R_{1} (A) \underset{1-1 onto}{⟶} ran G (A) \to R_{1} (A) \approx ran G (A)$
72		ennum	$⊢ R_{1} (A) \approx ran G (A) \to (R_{1} (A) \in dom card \leftrightarrow ran G (A) \in dom card)$
73	69 71 72	3syl	$⊢ φ \to (R_{1} (A) \in dom card \leftrightarrow ran G (A) \in dom card)$
74	67 73	mpbird	$⊢ φ \to R_{1} (A) \in dom card$

Metamath Proof Explorer

Theorem dfac12lem3

Proof