smfpimbor1lem1

Description: Every open set belongs to T . This is the second step in the proof of Proposition 121E (f) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimbor1lem1.s	$⊢ φ \to S \in SAlg$
	smfpimbor1lem1.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimbor1lem1.a	$⊢ D = dom F$
	smfpimbor1lem1.j	$⊢ J = topGen (ran (.))$
	smfpimbor1lem1.8	$⊢ φ \to G \in J$
	smfpimbor1lem1.t	$⊢ T = \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
Assertion	smfpimbor1lem1	$⊢ φ \to G \in T$

Proof

Step	Hyp	Ref	Expression
1		smfpimbor1lem1.s	$⊢ φ \to S \in SAlg$
2		smfpimbor1lem1.f	$⊢ φ \to F \in SMblFn (S)$
3		smfpimbor1lem1.a	$⊢ D = dom F$
4		smfpimbor1lem1.j	$⊢ J = topGen (ran (.))$
5		smfpimbor1lem1.8	$⊢ φ \to G \in J$
6		smfpimbor1lem1.t	$⊢ T = \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
7	4 5	tgqioo2	$⊢ φ \to \exists q (q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q)$
8		simprr	$⊢ (φ \land (q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q)) \to G = ⋃ q$
9	1 2 3 6	smfresal	$⊢ φ \to T \in SAlg$
10	9	adantr	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to T \in SAlg$
11		iooex	$⊢ (.) \in V$
12	11	imaexi	$⊢ (.) [ℚ \times ℚ] \in V$
13	12	a1i	$⊢ q \subseteq (.) [ℚ \times ℚ] \to (.) [ℚ \times ℚ] \in V$
14		id	$⊢ q \subseteq (.) [ℚ \times ℚ] \to q \subseteq (.) [ℚ \times ℚ]$
15	13 14	ssexd	$⊢ q \subseteq (.) [ℚ \times ℚ] \to q \in V$
16	15	adantl	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to q \in V$
17		simpr	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to q \subseteq (.) [ℚ \times ℚ]$
18		ioofun	$⊢ Fun (.)$
19	18	a1i	$⊢ q \in (.) [ℚ \times ℚ] \to Fun (.)$
20		id	$⊢ q \in (.) [ℚ \times ℚ] \to q \in (.) [ℚ \times ℚ]$
21		fvelima	$⊢ (Fun (.) \land q \in (.) [ℚ \times ℚ]) \to \exists p \in (ℚ \times ℚ) (.) (p) = q$
22	19 20 21	syl2anc	$⊢ q \in (.) [ℚ \times ℚ] \to \exists p \in (ℚ \times ℚ) (.) (p) = q$
23	22	adantl	$⊢ (φ \land q \in (.) [ℚ \times ℚ]) \to \exists p \in (ℚ \times ℚ) (.) (p) = q$
24		id	$⊢ (.) (p) = q \to (.) (p) = q$
25	24	eqcomd	$⊢ (.) (p) = q \to q = (.) (p)$
26	25	adantl	$⊢ (p \in (ℚ \times ℚ) \land (.) (p) = q) \to q = (.) (p)$
27		1st2nd2	$⊢ p \in (ℚ \times ℚ) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
28	27	fveq2d	$⊢ p \in (ℚ \times ℚ) \to (.) (p) = (.) (⟨1^{st} (p), 2^{nd} (p)⟩)$
29		df-ov	$⊢ (1^{st} (p), 2^{nd} (p)) = (.) (⟨1^{st} (p), 2^{nd} (p)⟩)$
30	29	eqcomi	$⊢ (.) (⟨1^{st} (p), 2^{nd} (p)⟩) = (1^{st} (p), 2^{nd} (p))$
31	30	a1i	$⊢ p \in (ℚ \times ℚ) \to (.) (⟨1^{st} (p), 2^{nd} (p)⟩) = (1^{st} (p), 2^{nd} (p))$
32	28 31	eqtrd	$⊢ p \in (ℚ \times ℚ) \to (.) (p) = (1^{st} (p), 2^{nd} (p))$
33	32	adantr	$⊢ (p \in (ℚ \times ℚ) \land (.) (p) = q) \to (.) (p) = (1^{st} (p), 2^{nd} (p))$
34	26 33	eqtrd	$⊢ (p \in (ℚ \times ℚ) \land (.) (p) = q) \to q = (1^{st} (p), 2^{nd} (p))$
35	34	3adant1	$⊢ (φ \land p \in (ℚ \times ℚ) \land (.) (p) = q) \to q = (1^{st} (p), 2^{nd} (p))$
36		ioossre	$⊢ (1^{st} (p), 2^{nd} (p)) \subseteq ℝ$
37		ovex	$⊢ (1^{st} (p), 2^{nd} (p)) \in V$
38	37	elpw	$⊢ (1^{st} (p), 2^{nd} (p)) \in 𝒫 ℝ \leftrightarrow (1^{st} (p), 2^{nd} (p)) \subseteq ℝ$
39	36 38	mpbir	$⊢ (1^{st} (p), 2^{nd} (p)) \in 𝒫 ℝ$
40	39	a1i	$⊢ (φ \land p \in (ℚ \times ℚ)) \to (1^{st} (p), 2^{nd} (p)) \in 𝒫 ℝ$
41	1	adantr	$⊢ (φ \land p \in (ℚ \times ℚ)) \to S \in SAlg$
42	2	adantr	$⊢ (φ \land p \in (ℚ \times ℚ)) \to F \in SMblFn (S)$
43		xp1st	$⊢ p \in (ℚ \times ℚ) \to 1^{st} (p) \in ℚ$
44	43	qred	$⊢ p \in (ℚ \times ℚ) \to 1^{st} (p) \in ℝ$
45	44	rexrd	$⊢ p \in (ℚ \times ℚ) \to 1^{st} (p) \in ℝ^{*}$
46	45	adantl	$⊢ (φ \land p \in (ℚ \times ℚ)) \to 1^{st} (p) \in ℝ^{*}$
47		xp2nd	$⊢ p \in (ℚ \times ℚ) \to 2^{nd} (p) \in ℚ$
48	47	qred	$⊢ p \in (ℚ \times ℚ) \to 2^{nd} (p) \in ℝ$
49	48	rexrd	$⊢ p \in (ℚ \times ℚ) \to 2^{nd} (p) \in ℝ^{*}$
50	49	adantl	$⊢ (φ \land p \in (ℚ \times ℚ)) \to 2^{nd} (p) \in ℝ^{*}$
51	41 42 3 46 50	smfpimioo	$⊢ (φ \land p \in (ℚ \times ℚ)) \to F^{-1} [(1^{st} (p), 2^{nd} (p))] \in (S ↾_{𝑡} D)$
52	40 51	jca	$⊢ (φ \land p \in (ℚ \times ℚ)) \to ((1^{st} (p), 2^{nd} (p)) \in 𝒫 ℝ \land F^{-1} [(1^{st} (p), 2^{nd} (p))] \in (S ↾_{𝑡} D))$
53		imaeq2	$⊢ e = (1^{st} (p), 2^{nd} (p)) \to F^{-1} [e] = F^{-1} [(1^{st} (p), 2^{nd} (p))]$
54	53	eleq1d	$⊢ e = (1^{st} (p), 2^{nd} (p)) \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [(1^{st} (p), 2^{nd} (p))] \in (S ↾_{𝑡} D))$
55	54 6	elrab2	$⊢ (1^{st} (p), 2^{nd} (p)) \in T \leftrightarrow ((1^{st} (p), 2^{nd} (p)) \in 𝒫 ℝ \land F^{-1} [(1^{st} (p), 2^{nd} (p))] \in (S ↾_{𝑡} D))$
56	52 55	sylibr	$⊢ (φ \land p \in (ℚ \times ℚ)) \to (1^{st} (p), 2^{nd} (p)) \in T$
57	56	3adant3	$⊢ (φ \land p \in (ℚ \times ℚ) \land (.) (p) = q) \to (1^{st} (p), 2^{nd} (p)) \in T$
58	35 57	eqeltrd	$⊢ (φ \land p \in (ℚ \times ℚ) \land (.) (p) = q) \to q \in T$
59	58	3exp	$⊢ φ \to (p \in (ℚ \times ℚ) \to ((.) (p) = q \to q \in T))$
60	59	rexlimdv	$⊢ φ \to (\exists p \in (ℚ \times ℚ) (.) (p) = q \to q \in T)$
61	60	adantr	$⊢ (φ \land q \in (.) [ℚ \times ℚ]) \to (\exists p \in (ℚ \times ℚ) (.) (p) = q \to q \in T)$
62	23 61	mpd	$⊢ (φ \land q \in (.) [ℚ \times ℚ]) \to q \in T$
63	62	ssd	$⊢ φ \to (.) [ℚ \times ℚ] \subseteq T$
64	63	adantr	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to (.) [ℚ \times ℚ] \subseteq T$
65	17 64	sstrd	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to q \subseteq T$
66	16 65	elpwd	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to q \in 𝒫 T$
67		ssdomg	$⊢ (.) [ℚ \times ℚ] \in V \to (q \subseteq (.) [ℚ \times ℚ] \to q ≼ (.) [ℚ \times ℚ])$
68	12 67	ax-mp	$⊢ q \subseteq (.) [ℚ \times ℚ] \to q ≼ (.) [ℚ \times ℚ]$
69		qct	$⊢ ℚ ≼ ω$
70	69 69	pm3.2i	$⊢ (ℚ ≼ ω \land ℚ ≼ ω)$
71		xpct	$⊢ (ℚ ≼ ω \land ℚ ≼ ω) \to (ℚ \times ℚ) ≼ ω$
72	70 71	ax-mp	$⊢ (ℚ \times ℚ) ≼ ω$
73		fimact	$⊢ ((ℚ \times ℚ) ≼ ω \land Fun (.)) \to (.) [ℚ \times ℚ] ≼ ω$
74	72 18 73	mp2an	$⊢ (.) [ℚ \times ℚ] ≼ ω$
75	74	a1i	$⊢ q \subseteq (.) [ℚ \times ℚ] \to (.) [ℚ \times ℚ] ≼ ω$
76		domtr	$⊢ (q ≼ (.) [ℚ \times ℚ] \land (.) [ℚ \times ℚ] ≼ ω) \to q ≼ ω$
77	68 75 76	syl2anc	$⊢ q \subseteq (.) [ℚ \times ℚ] \to q ≼ ω$
78	77	adantl	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to q ≼ ω$
79	10 66 78	salunicl	$⊢ (φ \land q \subseteq (.) [ℚ \times ℚ]) \to ⋃ q \in T$
80	79	adantrr	$⊢ (φ \land (q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q)) \to ⋃ q \in T$
81	8 80	eqeltrd	$⊢ (φ \land (q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q)) \to G \in T$
82	81	ex	$⊢ φ \to ((q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q) \to G \in T)$
83	82	exlimdv	$⊢ φ \to (\exists q (q \subseteq (.) [ℚ \times ℚ] \land G = ⋃ q) \to G \in T)$
84	7 83	mpd	$⊢ φ \to G \in T$

Metamath Proof Explorer

Theorem smfpimbor1lem1

Proof