grumnudlem

	Ref	Expression
Hypotheses	grumnudlem.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
	grumnudlem.2	$⊢ φ \to G \in Univ$
	grumnudlem.3	$⊢ F = \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)$
	grumnudlem.4	$⊢ (i \in G \land h \in G) \to (i F h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
	grumnudlem.5	$⊢ (h \in (F Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
Assertion	grumnudlem	$⊢ φ \to G \in M$

Proof

Step	Hyp	Ref	Expression
1		grumnudlem.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2		grumnudlem.2	$⊢ φ \to G \in Univ$
3		grumnudlem.3	$⊢ F = \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)$
4		grumnudlem.4	$⊢ (i \in G \land h \in G) \to (i F h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
5		grumnudlem.5	$⊢ (h \in (F Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
6		gruss	$⊢ (G \in Univ \land z \in G \land a \subseteq z) \to a \in G$
7	2 6	syl3an1	$⊢ (φ \land z \in G \land a \subseteq z) \to a \in G$
8	7	3expia	$⊢ (φ \land z \in G) \to (a \subseteq z \to a \in G)$
9	8	alrimiv	$⊢ (φ \land z \in G) \to \forall a (a \subseteq z \to a \in G)$
10		pwss	$⊢ 𝒫 z \subseteq G \leftrightarrow \forall a (a \subseteq z \to a \in G)$
11	9 10	sylibr	$⊢ (φ \land z \in G) \to 𝒫 z \subseteq G$
12		ssun1	$⊢ 𝒫 z \subseteq 𝒫 z \cup ⋃ (F Coll z)$
13		simp3	$⊢ (φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \to w = 𝒫 z \cup ⋃ (F Coll z)$
14	12 13	sseqtrrid	$⊢ (φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \to 𝒫 z \subseteq w$
15		simp1l3	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to w = 𝒫 z \cup ⋃ (F Coll z)$
16		simp1r	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to i \in z$
17		simpr	$⊢ (h = ⋃ v \land j = v) \to j = v$
18	17	unieqd	$⊢ (h = ⋃ v \land j = v) \to ⋃ j = ⋃ v$
19		simpl	$⊢ (h = ⋃ v \land j = v) \to h = ⋃ v$
20	18 19	eqtr4d	$⊢ (h = ⋃ v \land j = v) \to ⋃ j = h$
21	20	adantll	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to ⋃ j = h$
22		simpr	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to j = v$
23		simpll3	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to (i \in v \land v \in f)$
24	23	simprd	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to v \in f$
25	22 24	eqeltrd	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to j \in f$
26	23	simpld	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to i \in v$
27	26 22	eleqtrrd	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to i \in j$
28	21 25 27	3jca	$⊢ (((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \land j = v) \to (⋃ j = h \land j \in f \land i \in j)$
29		simpl2	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \to v \in G$
30	28 29	rr-spce	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h = ⋃ v) \to \exists j (⋃ j = h \land j \in f \land i \in j)$
31		simp1l1	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to φ$
32	31 2	syl	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to G \in Univ$
33		simp2	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to v \in G$
34		gruuni	$⊢ (G \in Univ \land v \in G) \to ⋃ v \in G$
35	32 33 34	syl2anc	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to ⋃ v \in G$
36	30 35	rspcime	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists h \in G \exists j (⋃ j = h \land j \in f \land i \in j)$
37		simpl1	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to φ$
38	37 2	syl	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to G \in Univ$
39		simpl2	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to z \in G$
40		simpr	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to i \in z$
41		gruel	$⊢ (G \in Univ \land z \in G \land i \in z) \to i \in G$
42	38 39 40 41	syl3anc	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to i \in G$
43	42	3ad2ant1	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to i \in G$
44	43 4	sylan	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in G) \to (i F h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
45	44	rexbidva	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to (\exists h \in G i F h \leftrightarrow \exists h \in G \exists j (⋃ j = h \land j \in f \land i \in j))$
46	36 45	mpbird	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists h \in G i F h$
47		rexex	$⊢ \exists h \in G i F h \to \exists h i F h$
48	46 47	syl	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists h i F h$
49	16 48	cpcoll2d	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists h \in (F Coll z) i F h$
50	32	adantr	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to G \in Univ$
51	39	3ad2ant1	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to z \in G$
52	51	adantr	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to z \in G$
53	2	adantr	$⊢ (φ \land z \in G) \to G \in Univ$
54		inss2	$⊢ \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G) \subseteq G \times G$
55	3 54	eqsstri	$⊢ F \subseteq G \times G$
56	55	a1i	$⊢ (φ \land z \in G) \to F \subseteq G \times G$
57		simpr	$⊢ (φ \land z \in G) \to z \in G$
58	53 56 57	grucollcld	$⊢ (φ \land z \in G) \to (F Coll z) \in G$
59	31 52 58	syl2an2r	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to (F Coll z) \in G$
60		simpr	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to h \in (F Coll z)$
61		gruel	$⊢ (G \in Univ \land (F Coll z) \in G \land h \in (F Coll z)) \to h \in G$
62	50 59 60 61	syl3anc	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to h \in G$
63	43 62 4	syl2an2r	$⊢ ((((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \land h \in (F Coll z)) \to (i F h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
64	63	rexbidva	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to (\exists h \in (F Coll z) i F h \leftrightarrow \exists h \in (F Coll z) \exists j (⋃ j = h \land j \in f \land i \in j))$
65	49 64	mpbid	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists h \in (F Coll z) \exists j (⋃ j = h \land j \in f \land i \in j)$
66		rexcom4	$⊢ \exists h \in (F Coll z) \exists j (⋃ j = h \land j \in f \land i \in j) \leftrightarrow \exists j \exists h \in (F Coll z) (⋃ j = h \land j \in f \land i \in j)$
67	5	rexlimiva	$⊢ \exists h \in (F Coll z) (⋃ j = h \land j \in f \land i \in j) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
68	67	exlimiv	$⊢ \exists j \exists h \in (F Coll z) (⋃ j = h \land j \in f \land i \in j) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
69	66 68	sylbi	$⊢ \exists h \in (F Coll z) \exists j (⋃ j = h \land j \in f \land i \in j) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
70	65 69	syl	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists u \in f (i \in u \land ⋃ u \in (F Coll z))$
71		elssuni	$⊢ ⋃ u \in (F Coll z) \to ⋃ u \subseteq ⋃ (F Coll z)$
72		ssun2	$⊢ ⋃ (F Coll z) \subseteq 𝒫 z \cup ⋃ (F Coll z)$
73	71 72	sstrdi	$⊢ ⋃ u \in (F Coll z) \to ⋃ u \subseteq 𝒫 z \cup ⋃ (F Coll z)$
74	73	adantl	$⊢ (w = 𝒫 z \cup ⋃ (F Coll z) \land ⋃ u \in (F Coll z)) \to ⋃ u \subseteq 𝒫 z \cup ⋃ (F Coll z)$
75		simpl	$⊢ (w = 𝒫 z \cup ⋃ (F Coll z) \land ⋃ u \in (F Coll z)) \to w = 𝒫 z \cup ⋃ (F Coll z)$
76	74 75	sseqtrrd	$⊢ (w = 𝒫 z \cup ⋃ (F Coll z) \land ⋃ u \in (F Coll z)) \to ⋃ u \subseteq w$
77	76	ex	$⊢ w = 𝒫 z \cup ⋃ (F Coll z) \to (⋃ u \in (F Coll z) \to ⋃ u \subseteq w)$
78	77	anim2d	$⊢ w = 𝒫 z \cup ⋃ (F Coll z) \to ((i \in u \land ⋃ u \in (F Coll z)) \to (i \in u \land ⋃ u \subseteq w))$
79	78	reximdv	$⊢ w = 𝒫 z \cup ⋃ (F Coll z) \to (\exists u \in f (i \in u \land ⋃ u \in (F Coll z)) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
80	15 70 79	sylc	$⊢ (((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \land v \in G \land (i \in v \land v \in f)) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)$
81	80	rexlimdv3a	$⊢ ((φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \land i \in z) \to (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
82	81	ralrimiva	$⊢ (φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \to \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
83	14 82	jca	$⊢ (φ \land z \in G \land w = 𝒫 z \cup ⋃ (F Coll z)) \to (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
84	83	3expa	$⊢ ((φ \land z \in G) \land w = 𝒫 z \cup ⋃ (F Coll z)) \to (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
85		grupw	$⊢ (G \in Univ \land z \in G) \to 𝒫 z \in G$
86	2 85	sylan	$⊢ (φ \land z \in G) \to 𝒫 z \in G$
87		gruuni	$⊢ (G \in Univ \land (F Coll z) \in G) \to ⋃ (F Coll z) \in G$
88	2 58 87	syl2an2r	$⊢ (φ \land z \in G) \to ⋃ (F Coll z) \in G$
89		gruun	$⊢ (G \in Univ \land 𝒫 z \in G \land ⋃ (F Coll z) \in G) \to 𝒫 z \cup ⋃ (F Coll z) \in G$
90	53 86 88 89	syl3anc	$⊢ (φ \land z \in G) \to 𝒫 z \cup ⋃ (F Coll z) \in G$
91	84 90	rspcime	$⊢ (φ \land z \in G) \to \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
92	91	alrimiv	$⊢ (φ \land z \in G) \to \forall f \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
93	11 92	jca	$⊢ (φ \land z \in G) \to (𝒫 z \subseteq G \land \forall f \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
94	93	ralrimiva	$⊢ φ \to \forall z \in G (𝒫 z \subseteq G \land \forall f \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
95	1	ismnu	$⊢ G \in Univ \to (G \in M \leftrightarrow \forall z \in G (𝒫 z \subseteq G \land \forall f \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$
96	2 95	syl	$⊢ φ \to (G \in M \leftrightarrow \forall z \in G (𝒫 z \subseteq G \land \forall f \exists w \in G (𝒫 z \subseteq w \land \forall i \in z (\exists v \in G (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$
97	94 96	mpbird	$⊢ φ \to G \in M$

Metamath Proof Explorer

Theorem grumnudlem

Proof