ptbasin

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015)

		Ref	Expression
	Hypothesis	ptbas.1	$⊢ B = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
	Assertion	ptbasin	$⊢ ((A \in V \land F : A ⟶ Top) \land (X \in B \land Y \in B)) \to X \cap Y \in B$

Proof

Step	Hyp	Ref	Expression
1		ptbas.1	$⊢ B = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
2	1	elpt	$⊢ X \in B \leftrightarrow \exists a ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y))$
3	1	elpt	$⊢ Y \in B \leftrightarrow \exists b ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y))$
4	2 3	anbi12i	$⊢ (X \in B \land Y \in B) \leftrightarrow (\exists a ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land \exists b ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y)))$
5		exdistrv	$⊢ \exists a \exists b (((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y))) \leftrightarrow (\exists a ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land \exists b ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y)))$
6	4 5	bitr4i	$⊢ (X \in B \land Y \in B) \leftrightarrow \exists a \exists b (((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y)))$
7		an4	$⊢ (((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y))) \leftrightarrow (((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))) \land (X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y)))$
8		an6	$⊢ ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))) \leftrightarrow ((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y)) \land (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))$
9		df-3an	$⊢ ((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y)) \land (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))) \leftrightarrow (((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))$
10	8 9	bitri	$⊢ ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))) \leftrightarrow (((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))$
11		reeanv	$⊢ \exists c \in Fin \exists d \in Fin (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \leftrightarrow (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))$
12		fveq2	$⊢ y = k \to a (y) = a (k)$
13		fveq2	$⊢ y = k \to b (y) = b (k)$
14	12 13	ineq12d	$⊢ y = k \to a (y) \cap b (y) = a (k) \cap b (k)$
15	14	cbvixpv	$⊢ \underset{y \in A}{⨉} (a (y) \cap b (y)) = \underset{k \in A}{⨉} (a (k) \cap b (k))$
16		simpl1l	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to A \in V$
17		unfi	$⊢ (c \in Fin \land d \in Fin) \to c \cup d \in Fin$
18	17	ad2antrl	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to c \cup d \in Fin$
19		simpl1r	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to F : A ⟶ Top$
20	19	ffvelrnda	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in A) \to F (k) \in Top$
21		simpl3l	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \forall y \in A a (y) \in F (y)$
22		fveq2	$⊢ y = k \to F (y) = F (k)$
23	12 22	eleq12d	$⊢ y = k \to (a (y) \in F (y) \leftrightarrow a (k) \in F (k))$
24	23	rspccva	$⊢ (\forall y \in A a (y) \in F (y) \land k \in A) \to a (k) \in F (k)$
25	21 24	sylan	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in A) \to a (k) \in F (k)$
26		simpl3r	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \forall y \in A b (y) \in F (y)$
27	13 22	eleq12d	$⊢ y = k \to (b (y) \in F (y) \leftrightarrow b (k) \in F (k))$
28	27	rspccva	$⊢ (\forall y \in A b (y) \in F (y) \land k \in A) \to b (k) \in F (k)$
29	26 28	sylan	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in A) \to b (k) \in F (k)$
30		inopn	$⊢ (F (k) \in Top \land a (k) \in F (k) \land b (k) \in F (k)) \to a (k) \cap b (k) \in F (k)$
31	20 25 29 30	syl3anc	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in A) \to a (k) \cap b (k) \in F (k)$
32		simprrl	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \forall y \in (A ∖ c) a (y) = ⋃ F (y)$
33		ssun1	$⊢ c \subseteq c \cup d$
34		sscon	$⊢ c \subseteq c \cup d \to A ∖ (c \cup d) \subseteq A ∖ c$
35	33 34	ax-mp	$⊢ A ∖ (c \cup d) \subseteq A ∖ c$
36	35	sseli	$⊢ k \in (A ∖ (c \cup d)) \to k \in (A ∖ c)$
37	22	unieqd	$⊢ y = k \to ⋃ F (y) = ⋃ F (k)$
38	12 37	eqeq12d	$⊢ y = k \to (a (y) = ⋃ F (y) \leftrightarrow a (k) = ⋃ F (k))$
39	38	rspccva	$⊢ (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land k \in (A ∖ c)) \to a (k) = ⋃ F (k)$
40	32 36 39	syl2an	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in (A ∖ (c \cup d))) \to a (k) = ⋃ F (k)$
41		simprrr	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \forall y \in (A ∖ d) b (y) = ⋃ F (y)$
42		ssun2	$⊢ d \subseteq c \cup d$
43		sscon	$⊢ d \subseteq c \cup d \to A ∖ (c \cup d) \subseteq A ∖ d$
44	42 43	ax-mp	$⊢ A ∖ (c \cup d) \subseteq A ∖ d$
45	44	sseli	$⊢ k \in (A ∖ (c \cup d)) \to k \in (A ∖ d)$
46	13 37	eqeq12d	$⊢ y = k \to (b (y) = ⋃ F (y) \leftrightarrow b (k) = ⋃ F (k))$
47	46	rspccva	$⊢ (\forall y \in (A ∖ d) b (y) = ⋃ F (y) \land k \in (A ∖ d)) \to b (k) = ⋃ F (k)$
48	41 45 47	syl2an	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in (A ∖ (c \cup d))) \to b (k) = ⋃ F (k)$
49	40 48	ineq12d	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in (A ∖ (c \cup d))) \to a (k) \cap b (k) = ⋃ F (k) \cap ⋃ F (k)$
50		inidm	$⊢ ⋃ F (k) \cap ⋃ F (k) = ⋃ F (k)$
51	49 50	syl6eq	$⊢ ((((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \land k \in (A ∖ (c \cup d))) \to a (k) \cap b (k) = ⋃ F (k)$
52	1 16 18 31 51	elptr2	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \underset{k \in A}{⨉} (a (k) \cap b (k)) \in B$
53	15 52	eqeltrid	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land ((c \in Fin \land d \in Fin) \land (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B$
54	53	expr	$⊢ (((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land (c \in Fin \land d \in Fin)) \to ((\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B)$
55	54	rexlimdvva	$⊢ ((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \to (\exists c \in Fin \exists d \in Fin (\forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B)$
56	11 55	syl5bir	$⊢ ((A \in V \land F : A ⟶ Top) \land (a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \to ((\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B)$
57	56	3expb	$⊢ ((A \in V \land F : A ⟶ Top) \land ((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y)))) \to ((\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B)$
58	57	impr	$⊢ ((A \in V \land F : A ⟶ Top) \land (((a Fn A \land b Fn A) \land (\forall y \in A a (y) \in F (y) \land \forall y \in A b (y) \in F (y))) \land (\exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B$
59	10 58	sylan2b	$⊢ ((A \in V \land F : A ⟶ Top) \land ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B$
60		ineq12	$⊢ (X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y)) \to X \cap Y = \underset{y \in A}{⨉} a (y) \cap \underset{y \in A}{⨉} b (y)$
61		ixpin	$⊢ \underset{y \in A}{⨉} (a (y) \cap b (y)) = \underset{y \in A}{⨉} a (y) \cap \underset{y \in A}{⨉} b (y)$
62	60 61	syl6eqr	$⊢ (X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y)) \to X \cap Y = \underset{y \in A}{⨉} (a (y) \cap b (y))$
63	62	eleq1d	$⊢ (X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y)) \to (X \cap Y \in B \leftrightarrow \underset{y \in A}{⨉} (a (y) \cap b (y)) \in B)$
64	59 63	syl5ibrcom	$⊢ ((A \in V \land F : A ⟶ Top) \land ((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)))) \to ((X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y)) \to X \cap Y \in B)$
65	64	expimpd	$⊢ (A \in V \land F : A ⟶ Top) \to ((((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land (b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y))) \land (X = \underset{y \in A}{⨉} a (y) \land Y = \underset{y \in A}{⨉} b (y))) \to X \cap Y \in B)$
66	7 65	syl5bi	$⊢ (A \in V \land F : A ⟶ Top) \to ((((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y))) \to X \cap Y \in B)$
67	66	exlimdvv	$⊢ (A \in V \land F : A ⟶ Top) \to (\exists a \exists b (((a Fn A \land \forall y \in A a (y) \in F (y) \land \exists c \in Fin \forall y \in (A ∖ c) a (y) = ⋃ F (y)) \land X = \underset{y \in A}{⨉} a (y)) \land ((b Fn A \land \forall y \in A b (y) \in F (y) \land \exists d \in Fin \forall y \in (A ∖ d) b (y) = ⋃ F (y)) \land Y = \underset{y \in A}{⨉} b (y))) \to X \cap Y \in B)$
68	6 67	syl5bi	$⊢ (A \in V \land F : A ⟶ Top) \to ((X \in B \land Y \in B) \to X \cap Y \in B)$
69	68	imp	$⊢ ((A \in V \land F : A ⟶ Top) \land (X \in B \land Y \in B)) \to X \cap Y \in B$

Metamath Proof Explorer

Theorem ptbasin

Proof