Step 
Hyp 
Ref 
Expression 
1 

1stmbfm.1 
⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra ) 
2 

1stmbfm.2 
⊢ ( 𝜑 → 𝑇 ∈ ∪ ran sigAlgebra ) 
3 

f1stres 
⊢ ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑆 
4 

sxuni 
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×_{s} 𝑇 ) ) 
5 
1 2 4

syl2anc 
⊢ ( 𝜑 → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×_{s} 𝑇 ) ) 
6 
5

feq2d 
⊢ ( 𝜑 → ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑆 ↔ ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_{s} 𝑇 ) ⟶ ∪ 𝑆 ) ) 
7 
3 6

mpbii 
⊢ ( 𝜑 → ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_{s} 𝑇 ) ⟶ ∪ 𝑆 ) 
8 

unielsiga 
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆 ) 
9 
1 8

syl 
⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝑆 ) 
10 

sxsiga 
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×_{s} 𝑇 ) ∈ ∪ ran sigAlgebra ) 
11 
1 2 10

syl2anc 
⊢ ( 𝜑 → ( 𝑆 ×_{s} 𝑇 ) ∈ ∪ ran sigAlgebra ) 
12 

unielsiga 
⊢ ( ( 𝑆 ×_{s} 𝑇 ) ∈ ∪ ran sigAlgebra → ∪ ( 𝑆 ×_{s} 𝑇 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
13 
11 12

syl 
⊢ ( 𝜑 → ∪ ( 𝑆 ×_{s} 𝑇 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
14 
9 13

elmapd 
⊢ ( 𝜑 → ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑆 ↑_{m} ∪ ( 𝑆 ×_{s} 𝑇 ) ) ↔ ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ∪ ( 𝑆 ×_{s} 𝑇 ) ⟶ ∪ 𝑆 ) ) 
15 
7 14

mpbird 
⊢ ( 𝜑 → ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑆 ↑_{m} ∪ ( 𝑆 ×_{s} 𝑇 ) ) ) 
16 

ffn 
⊢ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) : ( ∪ 𝑆 × ∪ 𝑇 ) ⟶ ∪ 𝑆 → ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) Fn ( ∪ 𝑆 × ∪ 𝑇 ) ) 
17 

elpreima 
⊢ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) Fn ( ∪ 𝑆 × ∪ 𝑇 ) → ( 𝑧 ∈ ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) ) ) 
18 
3 16 17

mp2b 
⊢ ( 𝑧 ∈ ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) ) 
19 

fvres 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) = ( 1^{st} ‘ 𝑧 ) ) 
20 
19

eleq1d 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ↔ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ) 
21 

1st2nd2 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ) 
22 

xp2nd 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) 
23 

elxp6 
⊢ ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ↔ ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ) ) 
24 

anass 
⊢ ( ( ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ↔ ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ) ) 
25 

an32 
⊢ ( ( ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ↔ ( ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ) 
26 
23 24 25

3bitr2i 
⊢ ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ↔ ( ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ) 
27 
26

baib 
⊢ ( ( 𝑧 = ⟨ ( 1^{st} ‘ 𝑧 ) , ( 2^{nd} ‘ 𝑧 ) ⟩ ∧ ( 2^{nd} ‘ 𝑧 ) ∈ ∪ 𝑇 ) → ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ↔ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ) 
28 
21 22 27

syl2anc 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ↔ ( 1^{st} ‘ 𝑧 ) ∈ 𝑎 ) ) 
29 
20 28

bitr4d 
⊢ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) → ( ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ↔ 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ) ) 
30 
29

pm5.32i 
⊢ ( ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ‘ 𝑧 ) ∈ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ) ) 
31 
18 30

bitri 
⊢ ( 𝑧 ∈ ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ) ) 
32 

sgon 
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ) 
33 

sigasspw 
⊢ ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) → 𝑆 ⊆ 𝒫 ∪ 𝑆 ) 
34 

pwssb 
⊢ ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀ 𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆 ) 
35 
34

biimpi 
⊢ ( 𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀ 𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆 ) 
36 
1 32 33 35

4syl 
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆 ) 
37 
36

r19.21bi 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ⊆ ∪ 𝑆 ) 
38 

xpss1 
⊢ ( 𝑎 ⊆ ∪ 𝑆 → ( 𝑎 × ∪ 𝑇 ) ⊆ ( ∪ 𝑆 × ∪ 𝑇 ) ) 
39 
37 38

syl 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 × ∪ 𝑇 ) ⊆ ( ∪ 𝑆 × ∪ 𝑇 ) ) 
40 
39

sseld 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) → 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ) ) 
41 
40

pm4.71rd 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ↔ ( 𝑧 ∈ ( ∪ 𝑆 × ∪ 𝑇 ) ∧ 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ) ) ) 
42 
31 41

bitr4id 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑧 ∈ ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ↔ 𝑧 ∈ ( 𝑎 × ∪ 𝑇 ) ) ) 
43 
42

eqrdv 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) = ( 𝑎 × ∪ 𝑇 ) ) 
44 
1

adantr 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) 
45 
2

adantr 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑇 ∈ ∪ ran sigAlgebra ) 
46 

simpr 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 ) 
47 

eqid 
⊢ ∪ 𝑇 = ∪ 𝑇 
48 

issgon 
⊢ ( 𝑇 ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ↔ ( 𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇 ) ) 
49 
2 47 48

sylanblrc 
⊢ ( 𝜑 → 𝑇 ∈ ( sigAlgebra ‘ ∪ 𝑇 ) ) 
50 

baselsiga 
⊢ ( 𝑇 ∈ ( sigAlgebra ‘ ∪ 𝑇 ) → ∪ 𝑇 ∈ 𝑇 ) 
51 
49 50

syl 
⊢ ( 𝜑 → ∪ 𝑇 ∈ 𝑇 ) 
52 
51

adantr 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ∪ 𝑇 ∈ 𝑇 ) 
53 

elsx 
⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) ∧ ( 𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇 ) ) → ( 𝑎 × ∪ 𝑇 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
54 
44 45 46 52 53

syl22anc 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 × ∪ 𝑇 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
55 
43 54

eqeltrd 
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
56 
55

ralrimiva 
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) 
57 
11 1

ismbfm 
⊢ ( 𝜑 → ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ( 𝑆 ×_{s} 𝑇 ) MblFnM 𝑆 ) ↔ ( ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ∪ 𝑆 ↑_{m} ∪ ( 𝑆 ×_{s} 𝑇 ) ) ∧ ∀ 𝑎 ∈ 𝑆 ( ^{◡} ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) “ 𝑎 ) ∈ ( 𝑆 ×_{s} 𝑇 ) ) ) ) 
58 
15 56 57

mpbir2and 
⊢ ( 𝜑 → ( 1^{st} ↾ ( ∪ 𝑆 × ∪ 𝑇 ) ) ∈ ( ( 𝑆 ×_{s} 𝑇 ) MblFnM 𝑆 ) ) 