ptcmplem4

	Ref	Expression
Hypotheses	ptcmp.1	$⊢ S = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
	ptcmp.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
	ptcmp.3	$⊢ φ \to A \in V$
	ptcmp.4	$⊢ φ \to F : A ⟶ Comp$
	ptcmp.5	$⊢ φ \to X \in (UFL \cap dom card)$
	ptcmplem2.5	$⊢ φ \to U \subseteq ran S$
	ptcmplem2.6	$⊢ φ \to X = ⋃ U$
	ptcmplem2.7	$⊢ φ \to \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
	ptcmplem3.8	$⊢ K = \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\}$
Assertion	ptcmplem4	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		ptcmp.1	$⊢ S = (k \in A, u \in F (k) ⟼ {(w \in X ⟼ w (k))}^{-1} [u])$
2		ptcmp.2	$⊢ X = \underset{n \in A}{⨉} ⋃ F (n)$
3		ptcmp.3	$⊢ φ \to A \in V$
4		ptcmp.4	$⊢ φ \to F : A ⟶ Comp$
5		ptcmp.5	$⊢ φ \to X \in (UFL \cap dom card)$
6		ptcmplem2.5	$⊢ φ \to U \subseteq ran S$
7		ptcmplem2.6	$⊢ φ \to X = ⋃ U$
8		ptcmplem2.7	$⊢ φ \to \neg \exists z \in (𝒫 U \cap Fin) X = ⋃ z$
9		ptcmplem3.8	$⊢ K = \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\}$
10	1 2 3 4 5 6 7 8 9	ptcmplem3	$⊢ φ \to \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$
11		simprl	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to f Fn A$
12		eldifi	$⊢ f (k) \in (⋃ F (k) ∖ ⋃ K) \to f (k) \in ⋃ F (k)$
13	12	ralimi	$⊢ \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall k \in A f (k) \in ⋃ F (k)$
14		fveq2	$⊢ n = k \to f (n) = f (k)$
15		fveq2	$⊢ n = k \to F (n) = F (k)$
16	15	unieqd	$⊢ n = k \to ⋃ F (n) = ⋃ F (k)$
17	14 16	eleq12d	$⊢ n = k \to (f (n) \in ⋃ F (n) \leftrightarrow f (k) \in ⋃ F (k))$
18	17	cbvralvw	$⊢ \forall n \in A f (n) \in ⋃ F (n) \leftrightarrow \forall k \in A f (k) \in ⋃ F (k)$
19	13 18	sylibr	$⊢ \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall n \in A f (n) \in ⋃ F (n)$
20	19	ad2antll	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to \forall n \in A f (n) \in ⋃ F (n)$
21		vex	$⊢ f \in V$
22	21	elixp	$⊢ f \in \underset{n \in A}{⨉} ⋃ F (n) \leftrightarrow (f Fn A \land \forall n \in A f (n) \in ⋃ F (n))$
23	11 20 22	sylanbrc	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to f \in \underset{n \in A}{⨉} ⋃ F (n)$
24	23 2	eleqtrrdi	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to f \in X$
25	7	adantr	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to X = ⋃ U$
26	24 25	eleqtrd	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to f \in ⋃ U$
27		eluni2	$⊢ f \in ⋃ U \leftrightarrow \exists v \in U f \in v$
28	26 27	sylib	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to \exists v \in U f \in v$
29		simplrr	$⊢ (((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \to f \in v$
30	29	adantr	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to f \in v$
31		simprr	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to v = {(w \in X ⟼ w (k))}^{-1} [u]$
32	30 31	eleqtrd	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to f \in {(w \in X ⟼ w (k))}^{-1} [u]$
33		fveq1	$⊢ w = f \to w (k) = f (k)$
34	33	eleq1d	$⊢ w = f \to (w (k) \in u \leftrightarrow f (k) \in u)$
35		eqid	$⊢ (w \in X ⟼ w (k)) = (w \in X ⟼ w (k))$
36	35	mptpreima	$⊢ {(w \in X ⟼ w (k))}^{-1} [u] = \{w \in X \| w (k) \in u\}$
37	34 36	elrab2	$⊢ f \in {(w \in X ⟼ w (k))}^{-1} [u] \leftrightarrow (f \in X \land f (k) \in u)$
38	37	simprbi	$⊢ f \in {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in u$
39	32 38	syl	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to f (k) \in u$
40		simprl	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to u \in F (k)$
41		simplrl	$⊢ (((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \to v \in U$
42	41	adantr	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to v \in U$
43	31 42	eqeltrrd	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to {(w \in X ⟼ w (k))}^{-1} [u] \in U$
44		rabid	$⊢ u \in \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\} \leftrightarrow (u \in F (k) \land {(w \in X ⟼ w (k))}^{-1} [u] \in U)$
45	40 43 44	sylanbrc	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to u \in \{u \in F (k) \| {(w \in X ⟼ w (k))}^{-1} [u] \in U\}$
46	45 9	eleqtrrdi	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to u \in K$
47		elunii	$⊢ (f (k) \in u \land u \in K) \to f (k) \in ⋃ K$
48	39 46 47	syl2anc	$⊢ ((((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (u \in F (k) \land v = {(w \in X ⟼ w (k))}^{-1} [u])) \to f (k) \in ⋃ K$
49	48	rexlimdvaa	$⊢ (((φ \land f Fn A) \land (v \in U \land f \in v)) \land (k \in A \land f (k) \in (⋃ F (k) ∖ ⋃ K))) \to (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K)$
50	49	expr	$⊢ (((φ \land f Fn A) \land (v \in U \land f \in v)) \land k \in A) \to (f (k) \in (⋃ F (k) ∖ ⋃ K) \to (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K))$
51	50	ralimdva	$⊢ ((φ \land f Fn A) \land (v \in U \land f \in v)) \to (\forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K))$
52	51	ex	$⊢ (φ \land f Fn A) \to ((v \in U \land f \in v) \to (\forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K)))$
53	52	com23	$⊢ (φ \land f Fn A) \to (\forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to ((v \in U \land f \in v) \to \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K)))$
54	53	impr	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to ((v \in U \land f \in v) \to \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K))$
55	54	imp	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (v \in U \land f \in v)) \to \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K)$
56	6	adantr	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to U \subseteq ran S$
57	56	sselda	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land v \in U) \to v \in ran S$
58	57	adantrr	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (v \in U \land f \in v)) \to v \in ran S$
59	1	rnmpo	$⊢ ran S = \{v \| \exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u]\}$
60	58 59	eleqtrdi	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (v \in U \land f \in v)) \to v \in \{v \| \exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u]\}$
61		abid	$⊢ v \in \{v \| \exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u]\} \leftrightarrow \exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u]$
62	60 61	sylib	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (v \in U \land f \in v)) \to \exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u]$
63		rexim	$⊢ \forall k \in A (\exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to f (k) \in ⋃ K) \to (\exists k \in A \exists u \in F (k) v = {(w \in X ⟼ w (k))}^{-1} [u] \to \exists k \in A f (k) \in ⋃ K)$
64	55 62 63	sylc	$⊢ ((φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \land (v \in U \land f \in v)) \to \exists k \in A f (k) \in ⋃ K$
65	28 64	rexlimddv	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to \exists k \in A f (k) \in ⋃ K$
66		eldifn	$⊢ f (k) \in (⋃ F (k) ∖ ⋃ K) \to \neg f (k) \in ⋃ K$
67	66	ralimi	$⊢ \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K) \to \forall k \in A \neg f (k) \in ⋃ K$
68	67	ad2antll	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to \forall k \in A \neg f (k) \in ⋃ K$
69		ralnex	$⊢ \forall k \in A \neg f (k) \in ⋃ K \leftrightarrow \neg \exists k \in A f (k) \in ⋃ K$
70	68 69	sylib	$⊢ (φ \land (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))) \to \neg \exists k \in A f (k) \in ⋃ K$
71	65 70	pm2.65da	$⊢ φ \to \neg (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$
72	71	nexdv	$⊢ φ \to \neg \exists f (f Fn A \land \forall k \in A f (k) \in (⋃ F (k) ∖ ⋃ K))$
73	10 72	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem ptcmplem4

Proof