tx1stc

Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	tx1stc	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( 𝑅 ×_t 𝑆 ) ∈ 1^stω )

Proof

Step	Hyp	Ref	Expression
1		1stctop	⊢ ( 𝑅 ∈ 1^stω → 𝑅 ∈ Top )
2		1stctop	⊢ ( 𝑆 ∈ 1^stω → 𝑆 ∈ Top )
3		txtop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×_t 𝑆 ) ∈ Top )
4	1 2 3	syl2an	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( 𝑅 ×_t 𝑆 ) ∈ Top )
5		eqid	⊢ ∪ 𝑅 = ∪ 𝑅
6	5	1stcclb	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑢 ∈ ∪ 𝑅 ) → ∃ 𝑎 ∈ 𝒫 𝑅 ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) )
7	6	ad2ant2r	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ∃ 𝑎 ∈ 𝒫 𝑅 ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) )
8		eqid	⊢ ∪ 𝑆 = ∪ 𝑆
9	8	1stcclb	⊢ ( ( 𝑆 ∈ 1^stω ∧ 𝑣 ∈ ∪ 𝑆 ) → ∃ 𝑏 ∈ 𝒫 𝑆 ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) )
10	9	ad2ant2l	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ∃ 𝑏 ∈ 𝒫 𝑆 ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) )
11		reeanv	⊢ ( ∃ 𝑎 ∈ 𝒫 𝑅 ∃ 𝑏 ∈ 𝒫 𝑆 ( ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ↔ ( ∃ 𝑎 ∈ 𝒫 𝑅 ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ∃ 𝑏 ∈ 𝒫 𝑆 ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) )
12		an4	⊢ ( ( ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ↔ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) )
13		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) )
14	13	ralrimivva	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) )
15	1 2 14	syl2an	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) )
16	15	adantr	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) )
17		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅 )
18		ssralv	⊢ ( 𝑎 ⊆ 𝑅 → ( ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
19	17 18	syl	⊢ ( 𝑎 ∈ 𝒫 𝑅 → ( ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
20		elpwi	⊢ ( 𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆 )
21		ssralv	⊢ ( 𝑏 ⊆ 𝑆 → ( ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
22	20 21	syl	⊢ ( 𝑏 ∈ 𝒫 𝑆 → ( ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
23	22	ralimdv	⊢ ( 𝑏 ∈ 𝒫 𝑆 → ( ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
24	19 23	sylan9	⊢ ( ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) → ( ∀ 𝑚 ∈ 𝑅 ∀ 𝑛 ∈ 𝑆 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ) )
25	16 24	mpan9	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) )
26		eqid	⊢ ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) = ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) )
27	26	fmpo	⊢ ( ∀ 𝑚 ∈ 𝑎 ∀ 𝑛 ∈ 𝑏 ( 𝑚 × 𝑛 ) ∈ ( 𝑅 ×_t 𝑆 ) ↔ ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) : ( 𝑎 × 𝑏 ) ⟶ ( 𝑅 ×_t 𝑆 ) )
28	25 27	sylib	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) : ( 𝑎 × 𝑏 ) ⟶ ( 𝑅 ×_t 𝑆 ) )
29	28	frnd	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ⊆ ( 𝑅 ×_t 𝑆 ) )
30		ovex	⊢ ( 𝑅 ×_t 𝑆 ) ∈ V
31	30	elpw2	⊢ ( ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ↔ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ⊆ ( 𝑅 ×_t 𝑆 ) )
32	29 31	sylibr	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) )
33	32	adantr	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) )
34		omelon	⊢ ω ∈ On
35		xpct	⊢ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) → ( 𝑎 × 𝑏 ) ≼ ω )
36		ondomen	⊢ ( ( ω ∈ On ∧ ( 𝑎 × 𝑏 ) ≼ ω ) → ( 𝑎 × 𝑏 ) ∈ dom card )
37	34 35 36	sylancr	⊢ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) → ( 𝑎 × 𝑏 ) ∈ dom card )
38		vex	⊢ 𝑚 ∈ V
39		vex	⊢ 𝑛 ∈ V
40	38 39	xpex	⊢ ( 𝑚 × 𝑛 ) ∈ V
41	26 40	fnmpoi	⊢ ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) Fn ( 𝑎 × 𝑏 )
42		dffn4	⊢ ( ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) Fn ( 𝑎 × 𝑏 ) ↔ ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) : ( 𝑎 × 𝑏 ) –onto→ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) )
43	41 42	mpbi	⊢ ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) : ( 𝑎 × 𝑏 ) –onto→ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) )
44		fodomnum	⊢ ( ( 𝑎 × 𝑏 ) ∈ dom card → ( ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) : ( 𝑎 × 𝑏 ) –onto→ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ( 𝑎 × 𝑏 ) ) )
45	37 43 44	mpisyl	⊢ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ( 𝑎 × 𝑏 ) )
46		domtr	⊢ ( ( ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ≼ ω ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω )
47	45 35 46	syl2anc	⊢ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω )
48	47	ad2antrl	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω )
49	1 2	anim12i	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) )
50	49	ad3antrrr	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) )
51		eltx	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ↔ ∀ 𝑤 ∈ 𝑧 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
52	50 51	syl	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ( 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ↔ ∀ 𝑤 ∈ 𝑧 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
53		eleq1	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ) )
54	53	anbi1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
55	54	2rexbidv	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
56	55	rspccv	⊢ ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
57		r19.27v	⊢ ( ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) → ∀ 𝑟 ∈ 𝑅 ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) )
58		r19.29	⊢ ( ( ∀ 𝑟 ∈ 𝑅 ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑟 ∈ 𝑅 ( ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
59		r19.29	⊢ ( ( ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑠 ∈ 𝑆 ( ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
60		opelxp	⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ↔ ( 𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠 ) )
61		pm3.35	⊢ ( ( 𝑢 ∈ 𝑟 ∧ ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) )
62		pm3.35	⊢ ( ( 𝑣 ∈ 𝑠 ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) )
63	61 62	anim12i	⊢ ( ( ( 𝑢 ∈ 𝑟 ∧ ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ( 𝑣 ∈ 𝑠 ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) )
64	63	an4s	⊢ ( ( ( 𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠 ) ∧ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) )
65	60 64	sylanb	⊢ ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) )
66	65	anim1i	⊢ ( ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
67	66	anasss	⊢ ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
68	67	an12s	⊢ ( ( ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
69	68	expl	⊢ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) → ( ( ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
70	69	reximdv	⊢ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) → ( ∃ 𝑠 ∈ 𝑆 ( ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
71	59 70	syl5	⊢ ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) → ( ( ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) )
72	71	impl	⊢ ( ( ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
73	72	reximi	⊢ ( ∃ 𝑟 ∈ 𝑅 ( ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
74	58 73	syl	⊢ ( ( ∀ 𝑟 ∈ 𝑅 ( ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
75	57 74	sylan	⊢ ( ( ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) )
76		reeanv	⊢ ( ∃ 𝑝 ∈ 𝑎 ∃ 𝑞 ∈ 𝑏 ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ↔ ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) )
77		simpr1l	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → 𝑝 ∈ 𝑎 )
78		simpr1r	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → 𝑞 ∈ 𝑏 )
79		eqidd	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑝 × 𝑞 ) = ( 𝑝 × 𝑞 ) )
80		xpeq1	⊢ ( 𝑚 = 𝑝 → ( 𝑚 × 𝑛 ) = ( 𝑝 × 𝑛 ) )
81	80	eqeq2d	⊢ ( 𝑚 = 𝑝 → ( ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) ↔ ( 𝑝 × 𝑞 ) = ( 𝑝 × 𝑛 ) ) )
82		xpeq2	⊢ ( 𝑛 = 𝑞 → ( 𝑝 × 𝑛 ) = ( 𝑝 × 𝑞 ) )
83	82	eqeq2d	⊢ ( 𝑛 = 𝑞 → ( ( 𝑝 × 𝑞 ) = ( 𝑝 × 𝑛 ) ↔ ( 𝑝 × 𝑞 ) = ( 𝑝 × 𝑞 ) ) )
84	81 83	rspc2ev	⊢ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ ( 𝑝 × 𝑞 ) = ( 𝑝 × 𝑞 ) ) → ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) )
85	77 78 79 84	syl3anc	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) )
86		vex	⊢ 𝑝 ∈ V
87		vex	⊢ 𝑞 ∈ V
88	86 87	xpex	⊢ ( 𝑝 × 𝑞 ) ∈ V
89		eqeq1	⊢ ( 𝑥 = ( 𝑝 × 𝑞 ) → ( 𝑥 = ( 𝑚 × 𝑛 ) ↔ ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) ) )
90	89	2rexbidv	⊢ ( 𝑥 = ( 𝑝 × 𝑞 ) → ( ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 𝑥 = ( 𝑚 × 𝑛 ) ↔ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) ) )
91	88 90	elab	⊢ ( ( 𝑝 × 𝑞 ) ∈ { 𝑥 ∣ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 𝑥 = ( 𝑚 × 𝑛 ) } ↔ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 ( 𝑝 × 𝑞 ) = ( 𝑚 × 𝑛 ) )
92	85 91	sylibr	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑝 × 𝑞 ) ∈ { 𝑥 ∣ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 𝑥 = ( 𝑚 × 𝑛 ) } )
93	26	rnmpo	⊢ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) = { 𝑥 ∣ ∃ 𝑚 ∈ 𝑎 ∃ 𝑛 ∈ 𝑏 𝑥 = ( 𝑚 × 𝑛 ) }
94	92 93	eleqtrrdi	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑝 × 𝑞 ) ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) )
95		simpr2	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) )
96		opelxpi	⊢ ( ( 𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞 ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) )
97	96	ad2ant2r	⊢ ( ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) )
98	95 97	syl	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) )
99		xpss12	⊢ ( ( 𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠 ) → ( 𝑝 × 𝑞 ) ⊆ ( 𝑟 × 𝑠 ) )
100	99	ad2ant2l	⊢ ( ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) → ( 𝑝 × 𝑞 ) ⊆ ( 𝑟 × 𝑠 ) )
101	95 100	syl	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑝 × 𝑞 ) ⊆ ( 𝑟 × 𝑠 ) )
102		simpr3	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑟 × 𝑠 ) ⊆ 𝑧 )
103	101 102	sstrd	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ( 𝑝 × 𝑞 ) ⊆ 𝑧 )
104		eleq2	⊢ ( 𝑤 = ( 𝑝 × 𝑞 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) ) )
105		sseq1	⊢ ( 𝑤 = ( 𝑝 × 𝑞 ) → ( 𝑤 ⊆ 𝑧 ↔ ( 𝑝 × 𝑞 ) ⊆ 𝑧 ) )
106	104 105	anbi12d	⊢ ( 𝑤 = ( 𝑝 × 𝑞 ) → ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) ∧ ( 𝑝 × 𝑞 ) ⊆ 𝑧 ) ) )
107	106	rspcev	⊢ ( ( ( 𝑝 × 𝑞 ) ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ∧ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑝 × 𝑞 ) ∧ ( 𝑝 × 𝑞 ) ⊆ 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
108	94 98 103 107	syl12anc	⊢ ( ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) ∧ ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
109	108	3exp2	⊢ ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ) → ( ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) → ( ( 𝑟 × 𝑠 ) ⊆ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
110	109	rexlimdvv	⊢ ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ∃ 𝑝 ∈ 𝑎 ∃ 𝑞 ∈ 𝑏 ( ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) → ( ( 𝑟 × 𝑠 ) ⊆ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
111	76 110	syl5bir	⊢ ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) → ( ( 𝑟 × 𝑠 ) ⊆ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
112	111	impd	⊢ ( ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
113	112	rexlimdvva	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ∧ ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
114	75 113	syl5	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) → ( ( ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
115	114	expd	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ) → ( ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
116	115	impr	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
117	56 116	syl9r	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ( ∀ 𝑤 ∈ 𝑧 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑤 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑧 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
118	52 117	sylbid	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ( 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
119	118	ralrimiv	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
120		breq1	⊢ ( 𝑦 = ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ( 𝑦 ≼ ω ↔ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω ) )
121		rexeq	⊢ ( 𝑦 = ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ( ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
122	121	imbi2d	⊢ ( 𝑦 = ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
123	122	ralbidv	⊢ ( 𝑦 = ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ( ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
124	120 123	anbi12d	⊢ ( 𝑦 = ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
125	124	rspcev	⊢ ( ( ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ∧ ( ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑚 ∈ 𝑎 , 𝑛 ∈ 𝑏 ↦ ( 𝑚 × 𝑛 ) ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
126	33 48 119 125	syl12anc	⊢ ( ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) ∧ ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
127	126	ex	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ( ( ( 𝑎 ≼ ω ∧ 𝑏 ≼ ω ) ∧ ( ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
128	12 127	syl5bi	⊢ ( ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆 ) ) → ( ( ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
129	128	rexlimdvva	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ( ∃ 𝑎 ∈ 𝒫 𝑅 ∃ 𝑏 ∈ 𝒫 𝑆 ( ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
130	11 129	syl5bir	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ( ( ∃ 𝑎 ∈ 𝒫 𝑅 ( 𝑎 ≼ ω ∧ ∀ 𝑟 ∈ 𝑅 ( 𝑢 ∈ 𝑟 → ∃ 𝑝 ∈ 𝑎 ( 𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟 ) ) ) ∧ ∃ 𝑏 ∈ 𝒫 𝑆 ( 𝑏 ≼ ω ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑣 ∈ 𝑠 → ∃ 𝑞 ∈ 𝑏 ( 𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
131	7 10 130	mp2and	⊢ ( ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) ∧ ( 𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆 ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
132	131	ralrimivva	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ∀ 𝑢 ∈ ∪ 𝑅 ∀ 𝑣 ∈ ∪ 𝑆 ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
133		eleq1	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑥 ∈ 𝑧 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 ) )
134		eleq1	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑥 ∈ 𝑤 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ) )
135	134	anbi1d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
136	135	rexbidv	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
137	133 136	imbi12d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
138	137	ralbidv	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
139	138	anbi2d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
140	139	rexbidv	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
141	140	ralxp	⊢ ( ∀ 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ∀ 𝑢 ∈ ∪ 𝑅 ∀ 𝑣 ∈ ∪ 𝑆 ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
142	132 141	sylibr	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ∀ 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
143	5 8	txuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×_t 𝑆 ) )
144	1 2 143	syl2an	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×_t 𝑆 ) )
145	144	raleqdv	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( ∀ 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ ∪ ( 𝑅 ×_t 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
146	142 145	mpbid	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ∀ 𝑥 ∈ ∪ ( 𝑅 ×_t 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
147		eqid	⊢ ∪ ( 𝑅 ×_t 𝑆 ) = ∪ ( 𝑅 ×_t 𝑆 )
148	147	is1stc2	⊢ ( ( 𝑅 ×_t 𝑆 ) ∈ 1^stω ↔ ( ( 𝑅 ×_t 𝑆 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( 𝑅 ×_t 𝑆 ) ∃ 𝑦 ∈ 𝒫 ( 𝑅 ×_t 𝑆 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
149	4 146 148	sylanbrc	⊢ ( ( 𝑅 ∈ 1^stω ∧ 𝑆 ∈ 1^stω ) → ( 𝑅 ×_t 𝑆 ) ∈ 1^stω )

Metamath Proof Explorer

Theorem tx1stc

Proof