Theorem tx1stc 23537

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

Assertion

Ref	Expression
tx1stc	⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)

Proof of Theorem tx1stc

Dummy variables 𝑎 𝑏 𝑚 𝑛 𝑝 𝑞 𝑟 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1stctop 23330	. . 3 ⊢ (𝑅 ∈ 1stω → 𝑅 ∈ Top)
2		1stctop 23330	. . 3 ⊢ (𝑆 ∈ 1stω → 𝑆 ∈ Top)
3		txtop 23456	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ Top)
5		eqid 2729	. . . . . . . 8 ⊢ ∪ 𝑅 = ∪ 𝑅
6	5	1stcclb 23331	. . . . . . 7 ⊢ ((𝑅 ∈ 1stω ∧ 𝑢 ∈ ∪ 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
7	6	ad2ant2r 747	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
8		eqid 2729	. . . . . . . 8 ⊢ ∪ 𝑆 = ∪ 𝑆
9	8	1stcclb 23331	. . . . . . 7 ⊢ ((𝑆 ∈ 1stω ∧ 𝑣 ∈ ∪ 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
10	9	ad2ant2l 746	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
11		reeanv 3209	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
12		an4 656	. . . . . . . . 9 ⊢ (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
13		txopn 23489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
14	13	ralrimivva 3180	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
15	1, 2, 14	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
16	15	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17		elpwi 4570	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅)
18		ssralv 4015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
19	17, 18	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20		elpwi 4570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆)
21		ssralv 4015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
23	22	ralimdv 3147	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
24	19, 23	sylan9 507	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
25	16, 24	mpan9 506	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
27	26	fmpo 8047	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
28	25, 27	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
29	28	frnd 6696	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30		ovex 7420	. . . . . . . . . . . . . 14 ⊢ (𝑅 ×t 𝑆) ∈ V
31	30	elpw2 5289	. . . . . . . . . . . . 13 ⊢ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
32	29, 31	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
33	32	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34		omelon 9599	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
35		xpct 9969	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
36		ondomen 9990	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
37	34, 35, 36	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
38		vex 3451	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ∈ V
39		vex 3451	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ V
40	38, 39	xpex 7729	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 × 𝑛) ∈ V
41	26, 40	fnmpoi 8049	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
42		dffn4 6778	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
43	41, 42	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
44		fodomnum 10010	. . . . . . . . . . . . . 14 ⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
45	37, 43, 44	mpisyl 21	. . . . . . . . . . . . 13 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
46		domtr 8978	. . . . . . . . . . . . 13 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
47	45, 35, 46	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
48	47	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
49	1, 2	anim12i 613	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
50	49	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
51		eltx 23455	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
52	50, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
53		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
54	53	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
55	54	2rexbidv 3202	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
56	55	rspccv 3585	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
57		r19.27v 3166	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
58		r19.29 3094	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
59		r19.29 3094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
60		opelxp 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠))
61		pm3.35 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))
62		pm3.35 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))
63	61, 62	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
64	63	an4s 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
65	60, 64	sylanb 581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
66	65	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
67	66	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
68	67	an12s 649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
69	68	expl 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
70	69	reximdv 3148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
71	59, 70	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
72	71	impl 455	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
73	72	reximi 3067	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
74	58, 73	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
75	57, 74	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
76		reeanv 3209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
77		simpr1l 1231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎)
78		simpr1r 1232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏)
79		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
80		xpeq1 5652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
81	80	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
82		xpeq2 5659	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
83	82	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
84	81, 83	rspc2ev 3601	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
85	77, 78, 79, 84	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
86		vex 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑝 ∈ V
87		vex 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑞 ∈ V
88	86, 87	xpex 7729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 × 𝑞) ∈ V
89		eqeq1 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
90	89	2rexbidv 3202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
91	88, 90	elab 3646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
92	85, 91	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)})
93	26	rnmpo 7522	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}
94	92, 93	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
95		simpr2 1196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
96		opelxpi 5675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
97	96	ad2ant2r 747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
98	95, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
99		xpss12 5653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
100	99	ad2ant2l 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
101	95, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
102		simpr3 1197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
103	101, 102	sstrd 3957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
104		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
105		sseq1 3972	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
106	104, 105	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
107	106	rspcev 3588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
108	94, 98, 103, 107	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
109	108	3exp2 1355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
110	109	rexlimdvv 3193	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
111	76, 110	biimtrrid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
112	111	impd 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
113	112	rexlimdvva 3194	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
114	75, 113	syl5 34	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
115	114	expd 415	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
116	115	impr 454	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
117	56, 116	syl9r 78	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
118	52, 117	sylbid 240	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
119	118	ralrimiv 3124	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
120		breq1 5110	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
121		rexeq 3295	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
122	121	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
123	122	ralbidv 3156	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
124	120, 123	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
125	124	rspcev 3588	. . . . . . . . . . 11 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
126	33, 48, 119, 125	syl12anc 836	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
127	126	ex 412	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
128	12, 127	biimtrid 242	. . . . . . . 8 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
129	128	rexlimdvva 3194	. . . . . . 7 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
130	11, 129	biimtrrid 243	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
131	7, 10, 130	mp2and 699	. . . . 5 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
132	131	ralrimivva 3180	. . . 4 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
133		eleq1 2816	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
134		eleq1 2816	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
135	134	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
136	135	rexbidv 3157	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
137	133, 136	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
138	137	ralbidv 3156	. . . . . . 7 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
139	138	anbi2d 630	. . . . . 6 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
140	139	rexbidv 3157	. . . . 5 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
141	140	ralxp 5805	. . . 4 ⊢ (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
142	132, 141	sylibr 234	. . 3 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
143	5, 8	txuni 23479	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
144	1, 2, 143	syl2an 596	. . 3 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
145	142, 144	raleqtrdv 3301	. 2 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
146		eqid 2729	. . 3 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
147	146	is1stc2 23329	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ 1stω ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
148	4, 145, 147	sylanbrc 583	1 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053   ⊆ wss 3914  𝒫 cpw 4563  ⟨cop 4595  ∪ cuni 4871   class class class wbr 5107   × cxp 5636  dom cdm 5638  ran crn 5639  Oncon0 6332   Fn wfn 6506  ⟶wf 6507  –onto→wfo 6509  (class class class)co 7387   ∈ cmpo 7389  ωcom 7842   ≼ cdom 8916  cardccrd 9888  Topctop 22780  1^stωc1stc 23324   ×_t ctx 23447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-oi 9463  df-card 9892  df-acn 9895  df-topgen 17406  df-top 22781  df-topon 22798  df-bases 22833  df-1stc 23326  df-tx 23449

This theorem is referenced by: (None)