pwfseqlem4a

	Ref	Expression
Hypotheses	pwfseqlem4.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
	pwfseqlem4.x	$⊢ φ \to X \subseteq A$
	pwfseqlem4.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
	pwfseqlem4.ps	$⊢ ψ \leftrightarrow ((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x)$
	pwfseqlem4.k	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x$
	pwfseqlem4.d	$⊢ D = G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
	pwfseqlem4.f	$⊢ F = (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
Assertion	pwfseqlem4a	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a F s \in A$

Proof

Step	Hyp	Ref	Expression
1		pwfseqlem4.g	$⊢ φ \to G : 𝒫 A \underset{1-1}{⟶} ⋃_{n \in ω} (A^{n})$
2		pwfseqlem4.x	$⊢ φ \to X \subseteq A$
3		pwfseqlem4.h	$⊢ φ \to H : ω \underset{1-1 onto}{⟶} X$
4		pwfseqlem4.ps	$⊢ ψ \leftrightarrow ((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x)$
5		pwfseqlem4.k	$⊢ (φ \land ψ) \to K : ⋃_{n \in ω} (x^{n}) \underset{1-1}{⟶} x$
6		pwfseqlem4.d	$⊢ D = G (\{w \in x \| (K^{-1} (w) \in ran G \land \neg w \in G^{-1} (K^{-1} (w)))\})$
7		pwfseqlem4.f	$⊢ F = (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
8		isfinite	$⊢ a \in Fin \leftrightarrow a ≺ ω$
9		simpr	$⊢ (φ \land a \in Fin) \to a \in Fin$
10		vex	$⊢ s \in V$
11	1 2 3 4 5 6 7	pwfseqlem2	$⊢ (a \in Fin \land s \in V) \to a F s = H (card (a))$
12	9 10 11	sylancl	$⊢ (φ \land a \in Fin) \to a F s = H (card (a))$
13		f1of	$⊢ H : ω \underset{1-1 onto}{⟶} X \to H : ω ⟶ X$
14	3 13	syl	$⊢ φ \to H : ω ⟶ X$
15	14 2	fssd	$⊢ φ \to H : ω ⟶ A$
16		ficardom	$⊢ a \in Fin \to card (a) \in ω$
17		ffvelcdm	$⊢ (H : ω ⟶ A \land card (a) \in ω) \to H (card (a)) \in A$
18	15 16 17	syl2an	$⊢ (φ \land a \in Fin) \to H (card (a)) \in A$
19	12 18	eqeltrd	$⊢ (φ \land a \in Fin) \to a F s \in A$
20	19	ex	$⊢ φ \to (a \in Fin \to a F s \in A)$
21	20	adantr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (a \in Fin \to a F s \in A)$
22	8 21	biimtrrid	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (a ≺ ω \to a F s \in A)$
23		omelon	$⊢ ω \in On$
24		onenon	$⊢ ω \in On \to ω \in dom card$
25	23 24	ax-mp	$⊢ ω \in dom card$
26		simpr3	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to s We a$
27	26	19.8ad	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to \exists s s We a$
28		ween	$⊢ a \in dom card \leftrightarrow \exists s s We a$
29	27 28	sylibr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a \in dom card$
30		domtri2	$⊢ (ω \in dom card \land a \in dom card) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
31	25 29 30	sylancr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \leftrightarrow \neg a ≺ ω)$
32		nfv	$⊢ Ⅎ r (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a))$
33		nfcv	$⊢ \underline{Ⅎ} r a$
34		nfmpo2	$⊢ \underline{Ⅎ} r (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
35	7 34	nfcxfr	$⊢ \underline{Ⅎ} r F$
36		nfcv	$⊢ \underline{Ⅎ} r s$
37	33 35 36	nfov	$⊢ \underline{Ⅎ} r (a F s)$
38	37	nfel1	$⊢ Ⅎ r a F s \in (A ∖ a)$
39	32 38	nfim	$⊢ Ⅎ r ((φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a))$
40		sseq1	$⊢ r = s \to (r \subseteq a \times a \leftrightarrow s \subseteq a \times a)$
41		weeq1	$⊢ r = s \to (r We a \leftrightarrow s We a)$
42	40 41	3anbi23d	$⊢ r = s \to ((a \subseteq A \land r \subseteq a \times a \land r We a) \leftrightarrow (a \subseteq A \land s \subseteq a \times a \land s We a))$
43	42	anbi1d	$⊢ r = s \to (((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a) \leftrightarrow ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a))$
44	43	anbi2d	$⊢ r = s \to ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \leftrightarrow (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)))$
45		oveq2	$⊢ r = s \to a F r = a F s$
46	45	eleq1d	$⊢ r = s \to (a F r \in (A ∖ a) \leftrightarrow a F s \in (A ∖ a))$
47	44 46	imbi12d	$⊢ r = s \to (((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)) \leftrightarrow ((φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a)))$
48		nfv	$⊢ Ⅎ x (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
49		nfcv	$⊢ \underline{Ⅎ} x a$
50		nfmpo1	$⊢ \underline{Ⅎ} x (x \in V, r \in V ⟼ if (x \in Fin, H (card (x)), D (⋂ \{z \in ω \| \neg D (z) \in x\})))$
51	7 50	nfcxfr	$⊢ \underline{Ⅎ} x F$
52		nfcv	$⊢ \underline{Ⅎ} x r$
53	49 51 52	nfov	$⊢ \underline{Ⅎ} x (a F r)$
54	53	nfel1	$⊢ Ⅎ x a F r \in (A ∖ a)$
55	48 54	nfim	$⊢ Ⅎ x ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a))$
56		sseq1	$⊢ x = a \to (x \subseteq A \leftrightarrow a \subseteq A)$
57		xpeq12	$⊢ (x = a \land x = a) \to x \times x = a \times a$
58	57	anidms	$⊢ x = a \to x \times x = a \times a$
59	58	sseq2d	$⊢ x = a \to (r \subseteq x \times x \leftrightarrow r \subseteq a \times a)$
60		weeq2	$⊢ x = a \to (r We x \leftrightarrow r We a)$
61	56 59 60	3anbi123d	$⊢ x = a \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (a \subseteq A \land r \subseteq a \times a \land r We a))$
62		breq2	$⊢ x = a \to (ω ≼ x \leftrightarrow ω ≼ a)$
63	61 62	anbi12d	$⊢ x = a \to (((x \subseteq A \land r \subseteq x \times x \land r We x) \land ω ≼ x) \leftrightarrow ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
64	4 63	bitrid	$⊢ x = a \to (ψ \leftrightarrow ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a))$
65	64	anbi2d	$⊢ x = a \to ((φ \land ψ) \leftrightarrow (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)))$
66		oveq1	$⊢ x = a \to x F r = a F r$
67		difeq2	$⊢ x = a \to A ∖ x = A ∖ a$
68	66 67	eleq12d	$⊢ x = a \to (x F r \in (A ∖ x) \leftrightarrow a F r \in (A ∖ a))$
69	65 68	imbi12d	$⊢ x = a \to (((φ \land ψ) \to x F r \in (A ∖ x)) \leftrightarrow ((φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)))$
70	1 2 3 4 5 6 7	pwfseqlem3	$⊢ (φ \land ψ) \to x F r \in (A ∖ x)$
71	55 69 70	chvarfv	$⊢ (φ \land ((a \subseteq A \land r \subseteq a \times a \land r We a) \land ω ≼ a)) \to a F r \in (A ∖ a)$
72	39 47 71	chvarfv	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in (A ∖ a)$
73	72	eldifad	$⊢ (φ \land ((a \subseteq A \land s \subseteq a \times a \land s We a) \land ω ≼ a)) \to a F s \in A$
74	73	expr	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (ω ≼ a \to a F s \in A)$
75	31 74	sylbird	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to (\neg a ≺ ω \to a F s \in A)$
76	22 75	pm2.61d	$⊢ (φ \land (a \subseteq A \land s \subseteq a \times a \land s We a)) \to a F s \in A$

Metamath Proof Explorer

Theorem pwfseqlem4a

Proof