stoweidlem35

Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem35.1	$⊢ Ⅎ t φ$
	stoweidlem35.2	$⊢ Ⅎ w φ$
	stoweidlem35.3	$⊢ Ⅎ h φ$
	stoweidlem35.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem35.5	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
	stoweidlem35.6	$⊢ G = (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
	stoweidlem35.7	$⊢ φ \to A \in V$
	stoweidlem35.8	$⊢ φ \to X \in Fin$
	stoweidlem35.9	$⊢ φ \to X \subseteq W$
	stoweidlem35.10	$⊢ φ \to T ∖ U \subseteq ⋃ X$
	stoweidlem35.11	$⊢ φ \to T ∖ U \neq \emptyset$
Assertion	stoweidlem35	$⊢ φ \to \exists m \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem35.1	$⊢ Ⅎ t φ$
2		stoweidlem35.2	$⊢ Ⅎ w φ$
3		stoweidlem35.3	$⊢ Ⅎ h φ$
4		stoweidlem35.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
5		stoweidlem35.5	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
6		stoweidlem35.6	$⊢ G = (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
7		stoweidlem35.7	$⊢ φ \to A \in V$
8		stoweidlem35.8	$⊢ φ \to X \in Fin$
9		stoweidlem35.9	$⊢ φ \to X \subseteq W$
10		stoweidlem35.10	$⊢ φ \to T ∖ U \subseteq ⋃ X$
11		stoweidlem35.11	$⊢ φ \to T ∖ U \neq \emptyset$
12	6	rnmptfi	$⊢ X \in Fin \to ran G \in Fin$
13	8 12	syl	$⊢ φ \to ran G \in Fin$
14		fnchoice	$⊢ ran G \in Fin \to \exists g (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))$
15	14	adantl	$⊢ (φ \land ran G \in Fin) \to \exists g (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))$
16		simprl	$⊢ (φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \to g Fn ran G$
17		nfmpt1	$⊢ \underline{Ⅎ} w (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
18	6 17	nfcxfr	$⊢ \underline{Ⅎ} w G$
19	18	nfrn	$⊢ \underline{Ⅎ} w ran G$
20	19	nfcri	$⊢ Ⅎ w k \in ran G$
21	2 20	nfan	$⊢ Ⅎ w (φ \land k \in ran G)$
22	9	sselda	$⊢ (φ \land w \in X) \to w \in W$
23	22 5	eleqtrdi	$⊢ (φ \land w \in X) \to w \in \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
24		rabid	$⊢ w \in \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow (w \in J \land \exists h \in Q w = \{t \in T \| 0 < h (t)\})$
25	23 24	sylib	$⊢ (φ \land w \in X) \to (w \in J \land \exists h \in Q w = \{t \in T \| 0 < h (t)\})$
26	25	simprd	$⊢ (φ \land w \in X) \to \exists h \in Q w = \{t \in T \| 0 < h (t)\}$
27		df-rex	$⊢ \exists h \in Q w = \{t \in T \| 0 < h (t)\} \leftrightarrow \exists h (h \in Q \land w = \{t \in T \| 0 < h (t)\})$
28	26 27	sylib	$⊢ (φ \land w \in X) \to \exists h (h \in Q \land w = \{t \in T \| 0 < h (t)\})$
29		rabid	$⊢ h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow (h \in Q \land w = \{t \in T \| 0 < h (t)\})$
30	29	exbii	$⊢ \exists h h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow \exists h (h \in Q \land w = \{t \in T \| 0 < h (t)\})$
31	28 30	sylibr	$⊢ (φ \land w \in X) \to \exists h h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
32	31	adantr	$⊢ ((φ \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to \exists h h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
33		nfv	$⊢ Ⅎ h w \in X$
34	3 33	nfan	$⊢ Ⅎ h (φ \land w \in X)$
35		nfrab1	$⊢ \underline{Ⅎ} h \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
36	35	nfeq2	$⊢ Ⅎ h k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
37	34 36	nfan	$⊢ Ⅎ h ((φ \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
38		eleq2	$⊢ k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \to (h \in k \leftrightarrow h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
39	38	biimprd	$⊢ k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \to (h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \to h \in k)$
40	39	adantl	$⊢ ((φ \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to (h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \to h \in k)$
41	37 40	eximd	$⊢ ((φ \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to (\exists h h \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \to \exists h h \in k)$
42	32 41	mpd	$⊢ ((φ \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to \exists h h \in k$
43	42	adantllr	$⊢ (((φ \land k \in ran G) \land w \in X) \land k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to \exists h h \in k$
44	6	elrnmpt	$⊢ k \in ran G \to (k \in ran G \leftrightarrow \exists w \in X k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
45	44	ibi	$⊢ k \in ran G \to \exists w \in X k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
46	45	adantl	$⊢ (φ \land k \in ran G) \to \exists w \in X k = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
47	21 43 46	r19.29af	$⊢ (φ \land k \in ran G) \to \exists h h \in k$
48		n0	$⊢ k \neq \emptyset \leftrightarrow \exists h h \in k$
49	47 48	sylibr	$⊢ (φ \land k \in ran G) \to k \neq \emptyset$
50	49	adantlr	$⊢ ((φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \land k \in ran G) \to k \neq \emptyset$
51		simplrr	$⊢ ((φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \land k \in ran G) \to \forall l \in ran G (l \neq \emptyset \to g (l) \in l)$
52		neeq1	$⊢ l = k \to (l \neq \emptyset \leftrightarrow k \neq \emptyset)$
53		fveq2	$⊢ l = k \to g (l) = g (k)$
54	53	eleq1d	$⊢ l = k \to (g (l) \in l \leftrightarrow g (k) \in l)$
55		eleq2	$⊢ l = k \to (g (k) \in l \leftrightarrow g (k) \in k)$
56	54 55	bitrd	$⊢ l = k \to (g (l) \in l \leftrightarrow g (k) \in k)$
57	52 56	imbi12d	$⊢ l = k \to ((l \neq \emptyset \to g (l) \in l) \leftrightarrow (k \neq \emptyset \to g (k) \in k))$
58	57	rspccva	$⊢ (\forall l \in ran G (l \neq \emptyset \to g (l) \in l) \land k \in ran G) \to (k \neq \emptyset \to g (k) \in k)$
59	51 58	sylancom	$⊢ ((φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \land k \in ran G) \to (k \neq \emptyset \to g (k) \in k)$
60	50 59	mpd	$⊢ ((φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \land k \in ran G) \to g (k) \in k$
61	60	ralrimiva	$⊢ (φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \to \forall k \in ran G g (k) \in k$
62		fveq2	$⊢ k = l \to g (k) = g (l)$
63	62	eleq1d	$⊢ k = l \to (g (k) \in k \leftrightarrow g (l) \in k)$
64		eleq2	$⊢ k = l \to (g (l) \in k \leftrightarrow g (l) \in l)$
65	63 64	bitrd	$⊢ k = l \to (g (k) \in k \leftrightarrow g (l) \in l)$
66	65	cbvralvw	$⊢ \forall k \in ran G g (k) \in k \leftrightarrow \forall l \in ran G g (l) \in l$
67	61 66	sylib	$⊢ (φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \to \forall l \in ran G g (l) \in l$
68	16 67	jca	$⊢ (φ \land (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l))) \to (g Fn ran G \land \forall l \in ran G g (l) \in l)$
69	68	ex	$⊢ φ \to ((g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l)) \to (g Fn ran G \land \forall l \in ran G g (l) \in l))$
70	69	adantr	$⊢ (φ \land ran G \in Fin) \to ((g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l)) \to (g Fn ran G \land \forall l \in ran G g (l) \in l))$
71	70	eximdv	$⊢ (φ \land ran G \in Fin) \to (\exists g (g Fn ran G \land \forall l \in ran G (l \neq \emptyset \to g (l) \in l)) \to \exists g (g Fn ran G \land \forall l \in ran G g (l) \in l))$
72	15 71	mpd	$⊢ (φ \land ran G \in Fin) \to \exists g (g Fn ran G \land \forall l \in ran G g (l) \in l)$
73	13 72	mpdan	$⊢ φ \to \exists g (g Fn ran G \land \forall l \in ran G g (l) \in l)$
74	73	ralrimivw	$⊢ φ \to \forall m \in ℕ \exists g (g Fn ran G \land \forall l \in ran G g (l) \in l)$
75		ssn0	$⊢ (T ∖ U \subseteq ⋃ X \land T ∖ U \neq \emptyset) \to ⋃ X \neq \emptyset$
76	10 11 75	syl2anc	$⊢ φ \to ⋃ X \neq \emptyset$
77	76	neneqd	$⊢ φ \to \neg ⋃ X = \emptyset$
78		unieq	$⊢ X = \emptyset \to ⋃ X = ⋃ \emptyset$
79		uni0	$⊢ ⋃ \emptyset = \emptyset$
80	78 79	eqtrdi	$⊢ X = \emptyset \to ⋃ X = \emptyset$
81	77 80	nsyl	$⊢ φ \to \neg X = \emptyset$
82		dm0rn0	$⊢ dom G = \emptyset \leftrightarrow ran G = \emptyset$
83	4 7	rabexd	$⊢ φ \to Q \in V$
84		nfrab1	$⊢ \underline{Ⅎ} h \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
85	4 84	nfcxfr	$⊢ \underline{Ⅎ} h Q$
86	85	rabexgf	$⊢ Q \in V \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
87	83 86	syl	$⊢ φ \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
88	87	adantr	$⊢ (φ \land w \in X) \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
89	2 88 6	fmptdf	$⊢ φ \to G : X ⟶ V$
90		dffn2	$⊢ G Fn X \leftrightarrow G : X ⟶ V$
91	89 90	sylibr	$⊢ φ \to G Fn X$
92	91	fndmd	$⊢ φ \to dom G = X$
93	92	eqeq1d	$⊢ φ \to (dom G = \emptyset \leftrightarrow X = \emptyset)$
94	82 93	bitr3id	$⊢ φ \to (ran G = \emptyset \leftrightarrow X = \emptyset)$
95	81 94	mtbird	$⊢ φ \to \neg ran G = \emptyset$
96		fz1f1o	$⊢ ran G \in Fin \to (ran G = \emptyset \lor (\|ran G\| \in ℕ \land \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G))$
97	13 96	syl	$⊢ φ \to (ran G = \emptyset \lor (\|ran G\| \in ℕ \land \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G))$
98	97	ord	$⊢ φ \to (\neg ran G = \emptyset \to (\|ran G\| \in ℕ \land \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G))$
99	95 98	mpd	$⊢ φ \to (\|ran G\| \in ℕ \land \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G)$
100		oveq2	$⊢ m = \|ran G\| \to (1 \dots m) = (1 \dots \|ran G\|)$
101	100	f1oeq2d	$⊢ m = \|ran G\| \to (f : (1 \dots m) \underset{1-1 onto}{⟶} ran G \leftrightarrow f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G)$
102	101	exbidv	$⊢ m = \|ran G\| \to (\exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G \leftrightarrow \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G)$
103	102	rspcev	$⊢ (\|ran G\| \in ℕ \land \exists f f : (1 \dots \|ran G\|) \underset{1-1 onto}{⟶} ran G) \to \exists m \in ℕ \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G$
104	99 103	syl	$⊢ φ \to \exists m \in ℕ \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G$
105		r19.29	$⊢ (\forall m \in ℕ \exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists m \in ℕ \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \to \exists m \in ℕ (\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
106	74 104 105	syl2anc	$⊢ φ \to \exists m \in ℕ (\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
107		exdistrv	$⊢ \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \leftrightarrow (\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
108	107	biimpri	$⊢ (\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \to \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
109	108	a1i	$⊢ φ \to ((\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \to \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
110	109	reximdv	$⊢ φ \to (\exists m \in ℕ (\exists g (g Fn ran G \land \forall l \in ran G g (l) \in l) \land \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \to \exists m \in ℕ \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
111	106 110	mpd	$⊢ φ \to \exists m \in ℕ \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
112		df-rex	$⊢ \exists m \in ℕ \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \leftrightarrow \exists m (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
113	111 112	sylib	$⊢ φ \to \exists m (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
114		ax-5	$⊢ m \in ℕ \to \forall g m \in ℕ$
115		19.29	$⊢ (\forall g m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g (m \in ℕ \land \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
116	114 115	sylan	$⊢ (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g (m \in ℕ \land \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
117		ax-5	$⊢ m \in ℕ \to \forall f m \in ℕ$
118		19.29	$⊢ (\forall f m \in ℕ \land \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists f (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
119	117 118	sylan	$⊢ (m \in ℕ \land \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists f (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
120	119	eximi	$⊢ \exists g (m \in ℕ \land \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g \exists f (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
121	116 120	syl	$⊢ (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g \exists f (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
122		df-3an	$⊢ (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G) \leftrightarrow ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
123	122	anbi2i	$⊢ (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \leftrightarrow (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
124	123	2exbii	$⊢ \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \leftrightarrow \exists g \exists f (m \in ℕ \land ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
125	121 124	sylibr	$⊢ (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
126	125	a1i	$⊢ φ \to ((m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)))$
127	126	eximdv	$⊢ φ \to (\exists m (m \in ℕ \land \exists g \exists f ((g Fn ran G \land \forall l \in ran G g (l) \in l) \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists m \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)))$
128	113 127	mpd	$⊢ φ \to \exists m \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
129	83	adantr	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to Q \in V$
130		simprl	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to m \in ℕ$
131		simprr1	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to g Fn ran G$
132		elex	$⊢ ran G \in Fin \to ran G \in V$
133	13 132	syl	$⊢ φ \to ran G \in V$
134	133	adantr	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to ran G \in V$
135		simprr2	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to \forall l \in ran G g (l) \in l$
136	56	rspccva	$⊢ (\forall l \in ran G g (l) \in l \land k \in ran G) \to g (k) \in k$
137	135 136	sylan	$⊢ ((φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \land k \in ran G) \to g (k) \in k$
138		simprr3	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to f : (1 \dots m) \underset{1-1 onto}{⟶} ran G$
139	10	adantr	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to T ∖ U \subseteq ⋃ X$
140		nfv	$⊢ Ⅎ t m \in ℕ$
141		nfcv	$⊢ \underline{Ⅎ} t g$
142		nfcv	$⊢ \underline{Ⅎ} t X$
143		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| 0 < h (t)\}$
144	143	nfeq2	$⊢ Ⅎ t w = \{t \in T \| 0 < h (t)\}$
145		nfv	$⊢ Ⅎ t h (Z) = 0$
146		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq h (t) \land h (t) \leq 1)$
147	145 146	nfan	$⊢ Ⅎ t (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))$
148		nfcv	$⊢ \underline{Ⅎ} t A$
149	147 148	nfrabw	$⊢ \underline{Ⅎ} t \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
150	4 149	nfcxfr	$⊢ \underline{Ⅎ} t Q$
151	144 150	nfrabw	$⊢ \underline{Ⅎ} t \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
152	142 151	nfmpt	$⊢ \underline{Ⅎ} t (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
153	6 152	nfcxfr	$⊢ \underline{Ⅎ} t G$
154	153	nfrn	$⊢ \underline{Ⅎ} t ran G$
155	141 154	nffn	$⊢ Ⅎ t g Fn ran G$
156		nfv	$⊢ Ⅎ t g (l) \in l$
157	154 156	nfralw	$⊢ Ⅎ t \forall l \in ran G g (l) \in l$
158		nfcv	$⊢ \underline{Ⅎ} t f$
159		nfcv	$⊢ \underline{Ⅎ} t (1 \dots m)$
160	158 159 154	nff1o	$⊢ Ⅎ t f : (1 \dots m) \underset{1-1 onto}{⟶} ran G$
161	155 157 160	nf3an	$⊢ Ⅎ t (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
162	140 161	nfan	$⊢ Ⅎ t (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
163	1 162	nfan	$⊢ Ⅎ t (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)))$
164		nfv	$⊢ Ⅎ w m \in ℕ$
165		nfcv	$⊢ \underline{Ⅎ} w g$
166	165 19	nffn	$⊢ Ⅎ w g Fn ran G$
167		nfv	$⊢ Ⅎ w g (l) \in l$
168	19 167	nfralw	$⊢ Ⅎ w \forall l \in ran G g (l) \in l$
169		nfcv	$⊢ \underline{Ⅎ} w f$
170		nfcv	$⊢ \underline{Ⅎ} w (1 \dots m)$
171	169 170 19	nff1o	$⊢ Ⅎ w f : (1 \dots m) \underset{1-1 onto}{⟶} ran G$
172	166 168 171	nf3an	$⊢ Ⅎ w (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)$
173	164 172	nfan	$⊢ Ⅎ w (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))$
174	2 173	nfan	$⊢ Ⅎ w (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)))$
175	6 129 130 131 134 137 138 139 163 174 85	stoweidlem27	$⊢ (φ \land (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G))) \to \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$
176	175	ex	$⊢ φ \to ((m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))))$
177	176	2eximdv	$⊢ φ \to (\exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists g \exists f \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))))$
178	177	eximdv	$⊢ φ \to (\exists m \exists g \exists f (m \in ℕ \land (g Fn ran G \land \forall l \in ran G g (l) \in l \land f : (1 \dots m) \underset{1-1 onto}{⟶} ran G)) \to \exists m \exists g \exists f \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))))$
179	128 178	mpd	$⊢ φ \to \exists m \exists g \exists f \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$
180		id	$⊢ \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))) \to \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$
181	180	exlimivv	$⊢ \exists g \exists f \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))) \to \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$
182	181	eximi	$⊢ \exists m \exists g \exists f \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t))) \to \exists m \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$
183	179 182	syl	$⊢ φ \to \exists m \exists q (m \in ℕ \land (q : (1 \dots m) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots m) 0 < q (i) (t)))$

Metamath Proof Explorer

Theorem stoweidlem35

Proof