dyadmbllem

	Ref	Expression
Hypotheses	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	dyadmbl.2	$⊢ G = \{z \in A \| \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)\}$
	dyadmbl.3	$⊢ φ \to A \subseteq ran F$
Assertion	dyadmbllem	$⊢ φ \to ⋃ [.] [A] = ⋃ [.] [G]$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		dyadmbl.2	$⊢ G = \{z \in A \| \forall w \in A ([.] (z) \subseteq [.] (w) \to z = w)\}$
3		dyadmbl.3	$⊢ φ \to A \subseteq ran F$
4		eluni2	$⊢ a \in ⋃ [.] [A] \leftrightarrow \exists i \in [.] [A] a \in i$
5		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
6		ffn	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.] Fn (ℝ^{} \times ℝ^{*})$
7	5 6	ax-mp	$⊢ [.] Fn (ℝ^{} \times ℝ^{})$
8	1	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
9		frn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to ran F \subseteq \leq \cap ℝ^{2}$
10	8 9	ax-mp	$⊢ ran F \subseteq \leq \cap ℝ^{2}$
11		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
12		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
13	11 12	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
14	10 13	sstri	$⊢ ran F \subseteq ℝ^{} \times ℝ^{}$
15	3 14	sstrdi	$⊢ φ \to A \subseteq ℝ^{} \times ℝ^{}$
16		eleq2	$⊢ i = [.] (t) \to (a \in i \leftrightarrow a \in [.] (t))$
17	16	rexima	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land A \subseteq ℝ^{} \times ℝ^{}) \to (\exists i \in [.] [A] a \in i \leftrightarrow \exists t \in A a \in [.] (t))$
18	7 15 17	sylancr	$⊢ φ \to (\exists i \in [.] [A] a \in i \leftrightarrow \exists t \in A a \in [.] (t))$
19		ssrab2	$⊢ \{a \in A \| [.] (t) \subseteq [.] (a)\} \subseteq A$
20	3	adantr	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to A \subseteq ran F$
21	19 20	sstrid	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to \{a \in A \| [.] (t) \subseteq [.] (a)\} \subseteq ran F$
22		simprl	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to t \in A$
23		ssid	$⊢ [.] (t) \subseteq [.] (t)$
24		fveq2	$⊢ a = t \to [.] (a) = [.] (t)$
25	24	sseq2d	$⊢ a = t \to ([.] (t) \subseteq [.] (a) \leftrightarrow [.] (t) \subseteq [.] (t))$
26	25	rspcev	$⊢ (t \in A \land [.] (t) \subseteq [.] (t)) \to \exists a \in A [.] (t) \subseteq [.] (a)$
27	22 23 26	sylancl	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to \exists a \in A [.] (t) \subseteq [.] (a)$
28		rabn0	$⊢ \{a \in A \| [.] (t) \subseteq [.] (a)\} \neq \emptyset \leftrightarrow \exists a \in A [.] (t) \subseteq [.] (a)$
29	27 28	sylibr	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to \{a \in A \| [.] (t) \subseteq [.] (a)\} \neq \emptyset$
30	1	dyadmax	$⊢ (\{a \in A \| [.] (t) \subseteq [.] (a)\} \subseteq ran F \land \{a \in A \| [.] (t) \subseteq [.] (a)\} \neq \emptyset) \to \exists m \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w)$
31	21 29 30	syl2anc	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to \exists m \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w)$
32		fveq2	$⊢ a = m \to [.] (a) = [.] (m)$
33	32	sseq2d	$⊢ a = m \to ([.] (t) \subseteq [.] (a) \leftrightarrow [.] (t) \subseteq [.] (m))$
34	33	elrab	$⊢ m \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \leftrightarrow (m \in A \land [.] (t) \subseteq [.] (m))$
35		simprlr	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to [.] (t) \subseteq [.] (m)$
36		simplrr	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to a \in [.] (t)$
37	35 36	sseldd	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to a \in [.] (m)$
38		simprll	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to m \in A$
39		fveq2	$⊢ a = w \to [.] (a) = [.] (w)$
40	39	sseq2d	$⊢ a = w \to ([.] (t) \subseteq [.] (a) \leftrightarrow [.] (t) \subseteq [.] (w))$
41	40	elrab	$⊢ w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \leftrightarrow (w \in A \land [.] (t) \subseteq [.] (w))$
42	41	imbi1i	$⊢ (w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \to ([.] (m) \subseteq [.] (w) \to m = w)) \leftrightarrow ((w \in A \land [.] (t) \subseteq [.] (w)) \to ([.] (m) \subseteq [.] (w) \to m = w))$
43		impexp	$⊢ ((w \in A \land [.] (t) \subseteq [.] (w)) \to ([.] (m) \subseteq [.] (w) \to m = w)) \leftrightarrow (w \in A \to ([.] (t) \subseteq [.] (w) \to ([.] (m) \subseteq [.] (w) \to m = w)))$
44	42 43	bitri	$⊢ (w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \to ([.] (m) \subseteq [.] (w) \to m = w)) \leftrightarrow (w \in A \to ([.] (t) \subseteq [.] (w) \to ([.] (m) \subseteq [.] (w) \to m = w)))$
45		impexp	$⊢ (([.] (t) \subseteq [.] (w) \land [.] (m) \subseteq [.] (w)) \to m = w) \leftrightarrow ([.] (t) \subseteq [.] (w) \to ([.] (m) \subseteq [.] (w) \to m = w))$
46		sstr2	$⊢ [.] (t) \subseteq [.] (m) \to ([.] (m) \subseteq [.] (w) \to [.] (t) \subseteq [.] (w))$
47	46	ad2antll	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to ([.] (m) \subseteq [.] (w) \to [.] (t) \subseteq [.] (w))$
48	47	ancrd	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to ([.] (m) \subseteq [.] (w) \to ([.] (t) \subseteq [.] (w) \land [.] (m) \subseteq [.] (w)))$
49	48	imim1d	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to ((([.] (t) \subseteq [.] (w) \land [.] (m) \subseteq [.] (w)) \to m = w) \to ([.] (m) \subseteq [.] (w) \to m = w))$
50	45 49	syl5bir	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to (([.] (t) \subseteq [.] (w) \to ([.] (m) \subseteq [.] (w) \to m = w)) \to ([.] (m) \subseteq [.] (w) \to m = w))$
51	50	imim2d	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to ((w \in A \to ([.] (t) \subseteq [.] (w) \to ([.] (m) \subseteq [.] (w) \to m = w))) \to (w \in A \to ([.] (m) \subseteq [.] (w) \to m = w)))$
52	44 51	syl5bi	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to ((w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \to ([.] (m) \subseteq [.] (w) \to m = w)) \to (w \in A \to ([.] (m) \subseteq [.] (w) \to m = w)))$
53	52	ralimdv2	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land (m \in A \land [.] (t) \subseteq [.] (m))) \to (\forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w) \to \forall w \in A ([.] (m) \subseteq [.] (w) \to m = w))$
54	53	impr	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to \forall w \in A ([.] (m) \subseteq [.] (w) \to m = w)$
55		fveq2	$⊢ z = m \to [.] (z) = [.] (m)$
56	55	sseq1d	$⊢ z = m \to ([.] (z) \subseteq [.] (w) \leftrightarrow [.] (m) \subseteq [.] (w))$
57		equequ1	$⊢ z = m \to (z = w \leftrightarrow m = w)$
58	56 57	imbi12d	$⊢ z = m \to (([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow ([.] (m) \subseteq [.] (w) \to m = w))$
59	58	ralbidv	$⊢ z = m \to (\forall w \in A ([.] (z) \subseteq [.] (w) \to z = w) \leftrightarrow \forall w \in A ([.] (m) \subseteq [.] (w) \to m = w))$
60	59 2	elrab2	$⊢ m \in G \leftrightarrow (m \in A \land \forall w \in A ([.] (m) \subseteq [.] (w) \to m = w))$
61	38 54 60	sylanbrc	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to m \in G$
62		ffun	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*} \to Fun [.]$
63	5 62	ax-mp	$⊢ Fun [.]$
64	2	ssrab3	$⊢ G \subseteq A$
65	64 15	sstrid	$⊢ φ \to G \subseteq ℝ^{} \times ℝ^{}$
66	5	fdmi	$⊢ dom [.] = ℝ^{} \times ℝ^{}$
67	65 66	sseqtrrdi	$⊢ φ \to G \subseteq dom [.]$
68	67	ad2antrr	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to G \subseteq dom [.]$
69		funfvima2	$⊢ (Fun [.] \land G \subseteq dom [.]) \to (m \in G \to [.] (m) \in [.] [G])$
70	63 68 69	sylancr	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to (m \in G \to [.] (m) \in [.] [G])$
71	61 70	mpd	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to [.] (m) \in [.] [G]$
72		elunii	$⊢ (a \in [.] (m) \land [.] (m) \in [.] [G]) \to a \in ⋃ [.] [G]$
73	37 71 72	syl2anc	$⊢ ((φ \land (t \in A \land a \in [.] (t))) \land ((m \in A \land [.] (t) \subseteq [.] (m)) \land \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w))) \to a \in ⋃ [.] [G]$
74	73	exp32	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to ((m \in A \land [.] (t) \subseteq [.] (m)) \to (\forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w) \to a \in ⋃ [.] [G]))$
75	34 74	syl5bi	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to (m \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \to (\forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w) \to a \in ⋃ [.] [G]))$
76	75	rexlimdv	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to (\exists m \in \{a \in A \| [.] (t) \subseteq [.] (a)\} \forall w \in \{a \in A \| [.] (t) \subseteq [.] (a)\} ([.] (m) \subseteq [.] (w) \to m = w) \to a \in ⋃ [.] [G])$
77	31 76	mpd	$⊢ (φ \land (t \in A \land a \in [.] (t))) \to a \in ⋃ [.] [G]$
78	77	rexlimdvaa	$⊢ φ \to (\exists t \in A a \in [.] (t) \to a \in ⋃ [.] [G])$
79	18 78	sylbid	$⊢ φ \to (\exists i \in [.] [A] a \in i \to a \in ⋃ [.] [G])$
80	4 79	syl5bi	$⊢ φ \to (a \in ⋃ [.] [A] \to a \in ⋃ [.] [G])$
81	80	ssrdv	$⊢ φ \to ⋃ [.] [A] \subseteq ⋃ [.] [G]$
82		imass2	$⊢ G \subseteq A \to [.] [G] \subseteq [.] [A]$
83	64 82	ax-mp	$⊢ [.] [G] \subseteq [.] [A]$
84		uniss	$⊢ [.] [G] \subseteq [.] [A] \to ⋃ [.] [G] \subseteq ⋃ [.] [A]$
85	83 84	mp1i	$⊢ φ \to ⋃ [.] [G] \subseteq ⋃ [.] [A]$
86	81 85	eqssd	$⊢ φ \to ⋃ [.] [A] = ⋃ [.] [G]$

Metamath Proof Explorer

Theorem dyadmbllem

Proof