Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimbor1lem1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimbor1lem1.a	⊢ 𝐷 = dom 𝐹
	smfpimbor1lem1.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	smfpimbor1lem1.8	⊢ ( 𝜑 → 𝐺 ∈ 𝐽 )
	smfpimbor1lem1.t	⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
Assertion	smfpimbor1lem1	⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		smfpimbor1lem1.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfpimbor1lem1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfpimbor1lem1.a	⊢ 𝐷 = dom 𝐹
4		smfpimbor1lem1.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
5		smfpimbor1lem1.8	⊢ ( 𝜑 → 𝐺 ∈ 𝐽 )
6		smfpimbor1lem1.t	⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
7	4 5	tgqioo2	⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) ) → 𝐺 = ∪ 𝑞 )
9	1 2 3 6	smfresal	⊢ ( 𝜑 → 𝑇 ∈ SAlg )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑇 ∈ SAlg )
11		iooex	⊢ (,) ∈ V
12	11	imaexi	⊢ ( (,) “ ( ℚ × ℚ ) ) ∈ V
13	12	a1i	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → ( (,) “ ( ℚ × ℚ ) ) ∈ V )
14		id	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) )
15	13 14	ssexd	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ∈ V )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ∈ V )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) )
18		ioofun	⊢ Fun (,)
19	18	a1i	⊢ ( 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) → Fun (,) )
20		id	⊢ ( 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) )
21		fvelima	⊢ ( ( Fun (,) ∧ 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) ) → ∃ 𝑝 ∈ ( ℚ × ℚ ) ( (,) ‘ 𝑝 ) = 𝑞 )
22	19 20 21	syl2anc	⊢ ( 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) → ∃ 𝑝 ∈ ( ℚ × ℚ ) ( (,) ‘ 𝑝 ) = 𝑞 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) ) → ∃ 𝑝 ∈ ( ℚ × ℚ ) ( (,) ‘ 𝑝 ) = 𝑞 )
24		id	⊢ ( ( (,) ‘ 𝑝 ) = 𝑞 → ( (,) ‘ 𝑝 ) = 𝑞 )
25	24	eqcomd	⊢ ( ( (,) ‘ 𝑝 ) = 𝑞 → 𝑞 = ( (,) ‘ 𝑝 ) )
26	25	adantl	⊢ ( ( 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → 𝑞 = ( (,) ‘ 𝑝 ) )
27		1st2nd2	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
28	27	fveq2d	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( (,) ‘ 𝑝 ) = ( (,) ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ) )
29		df-ov	⊢ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) = ( (,) ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
30	29	eqcomi	⊢ ( (,) ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ) = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) )
31	30	a1i	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( (,) ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ) = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) )
32	28 31	eqtrd	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( (,) ‘ 𝑝 ) = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) )
33	32	adantr	⊢ ( ( 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → ( (,) ‘ 𝑝 ) = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) )
34	26 33	eqtrd	⊢ ( ( 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → 𝑞 = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) )
35	34	3adant1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → 𝑞 = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) )
36		ioossre	⊢ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ⊆ ℝ
37		ovex	⊢ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ V
38	37	elpw	⊢ ( ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝒫 ℝ ↔ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ⊆ ℝ )
39	36 38	mpbir	⊢ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝒫 ℝ
40	39	a1i	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝒫 ℝ )
41	1	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → 𝑆 ∈ SAlg )
42	2	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
43		xp1st	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 1st ‘ 𝑝 ) ∈ ℚ )
44	43	qred	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 1st ‘ 𝑝 ) ∈ ℝ )
45	44	rexrd	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 1st ‘ 𝑝 ) ∈ ℝ* )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( 1st ‘ 𝑝 ) ∈ ℝ* )
47		xp2nd	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 2nd ‘ 𝑝 ) ∈ ℚ )
48	47	qred	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 2nd ‘ 𝑝 ) ∈ ℝ )
49	48	rexrd	⊢ ( 𝑝 ∈ ( ℚ × ℚ ) → ( 2nd ‘ 𝑝 ) ∈ ℝ* )
50	49	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( 2nd ‘ 𝑝 ) ∈ ℝ* )
51	41 42 3 46 50	smfpimioo	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( ◡ 𝐹 “ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
52	40 51	jca	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
53		imaeq2	⊢ ( 𝑒 = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ) )
54	53	eleq1d	⊢ ( 𝑒 = ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
55	54 6	elrab2	⊢ ( ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝑇 ↔ ( ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
56	52 55	sylibr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ) → ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝑇 )
57	56	3adant3	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → ( ( 1st ‘ 𝑝 ) (,) ( 2nd ‘ 𝑝 ) ) ∈ 𝑇 )
58	35 57	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ℚ × ℚ ) ∧ ( (,) ‘ 𝑝 ) = 𝑞 ) → 𝑞 ∈ 𝑇 )
59	58	3exp	⊢ ( 𝜑 → ( 𝑝 ∈ ( ℚ × ℚ ) → ( ( (,) ‘ 𝑝 ) = 𝑞 → 𝑞 ∈ 𝑇 ) ) )
60	59	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( ℚ × ℚ ) ( (,) ‘ 𝑝 ) = 𝑞 → 𝑞 ∈ 𝑇 ) )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) ) → ( ∃ 𝑝 ∈ ( ℚ × ℚ ) ( (,) ‘ 𝑝 ) = 𝑞 → 𝑞 ∈ 𝑇 ) )
62	23 61	mpd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ∈ 𝑇 )
63	62	ssd	⊢ ( 𝜑 → ( (,) “ ( ℚ × ℚ ) ) ⊆ 𝑇 )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → ( (,) “ ( ℚ × ℚ ) ) ⊆ 𝑇 )
65	17 64	sstrd	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ⊆ 𝑇 )
66	16 65	elpwd	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ∈ 𝒫 𝑇 )
67		ssdomg	⊢ ( ( (,) “ ( ℚ × ℚ ) ) ∈ V → ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ≼ ( (,) “ ( ℚ × ℚ ) ) ) )
68	12 67	ax-mp	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ≼ ( (,) “ ( ℚ × ℚ ) ) )
69		qct	⊢ ℚ ≼ ω
70	69 69	pm3.2i	⊢ ( ℚ ≼ ω ∧ ℚ ≼ ω )
71		xpct	⊢ ( ( ℚ ≼ ω ∧ ℚ ≼ ω ) → ( ℚ × ℚ ) ≼ ω )
72	70 71	ax-mp	⊢ ( ℚ × ℚ ) ≼ ω
73		fimact	⊢ ( ( ( ℚ × ℚ ) ≼ ω ∧ Fun (,) ) → ( (,) “ ( ℚ × ℚ ) ) ≼ ω )
74	72 18 73	mp2an	⊢ ( (,) “ ( ℚ × ℚ ) ) ≼ ω
75	74	a1i	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → ( (,) “ ( ℚ × ℚ ) ) ≼ ω )
76		domtr	⊢ ( ( 𝑞 ≼ ( (,) “ ( ℚ × ℚ ) ) ∧ ( (,) “ ( ℚ × ℚ ) ) ≼ ω ) → 𝑞 ≼ ω )
77	68 75 76	syl2anc	⊢ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑞 ≼ ω )
78	77	adantl	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → 𝑞 ≼ ω )
79	10 66 78	salunicl	⊢ ( ( 𝜑 ∧ 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ) → ∪ 𝑞 ∈ 𝑇 )
80	79	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) ) → ∪ 𝑞 ∈ 𝑇 )
81	8 80	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) ) → 𝐺 ∈ 𝑇 )
82	81	ex	⊢ ( 𝜑 → ( ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) → 𝐺 ∈ 𝑇 ) )
83	82	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑞 ( 𝑞 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐺 = ∪ 𝑞 ) → 𝐺 ∈ 𝑇 ) )
84	7 83	mpd	⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )