Step | Hyp | Ref
| Expression |
1 | | imambfm.2 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
2 | 1 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑆 ∈ ∪ ran
sigAlgebra) |
3 | | imambfm.3 |
. . . . . 6
⊢ (𝜑 → 𝑇 = (sigaGen‘𝐾)) |
4 | | imambfm.1 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ V) |
5 | 4 | sgsiga 31822 |
. . . . . 6
⊢ (𝜑 → (sigaGen‘𝐾) ∈ ∪ ran sigAlgebra) |
6 | 3, 5 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ∪ ran
sigAlgebra) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝑇 ∈ ∪ ran
sigAlgebra) |
8 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹 ∈ (𝑆MblFnM𝑇)) |
9 | 2, 7, 8 | mbfmf 31934 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
10 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑆 ∈ ∪ ran
sigAlgebra) |
11 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑇 ∈ ∪ ran
sigAlgebra) |
12 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝐹 ∈ (𝑆MblFnM𝑇)) |
13 | | sssigagen 31825 |
. . . . . . . . 9
⊢ (𝐾 ∈ V → 𝐾 ⊆ (sigaGen‘𝐾)) |
14 | 4, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ⊆ (sigaGen‘𝐾)) |
15 | 14, 3 | sseqtrrd 3942 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ⊆ 𝑇) |
16 | 15 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝐾 ⊆ 𝑇) |
17 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾) |
18 | 16, 17 | sseldd 3902 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝑇) |
19 | 10, 11, 12, 18 | mbfmcnvima 31936 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ∈ 𝑆) |
20 | 19 | ralrimiva 3105 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆) |
21 | 9, 20 | jca 515 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑆MblFnM𝑇)) → (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) |
22 | | unielsiga 31808 |
. . . . . 6
⊢ (𝑇 ∈ ∪ ran sigAlgebra → ∪ 𝑇 ∈ 𝑇) |
23 | 6, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑇
∈ 𝑇) |
24 | 23 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑇 ∈ 𝑇) |
25 | | unielsiga 31808 |
. . . . . 6
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆) |
26 | 1, 25 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ 𝑆
∈ 𝑆) |
27 | 26 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑆 ∈ 𝑆) |
28 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
29 | | elmapg 8521 |
. . . . 5
⊢ ((∪ 𝑇
∈ 𝑇 ∧ ∪ 𝑆
∈ 𝑆) → (𝐹 ∈ (∪ 𝑇
↑m ∪ 𝑆) ↔ 𝐹:∪ 𝑆⟶∪ 𝑇)) |
30 | 29 | biimpar 481 |
. . . 4
⊢ (((∪ 𝑇
∈ 𝑇 ∧ ∪ 𝑆
∈ 𝑆) ∧ 𝐹:∪
𝑆⟶∪ 𝑇)
→ 𝐹 ∈ (∪ 𝑇
↑m ∪ 𝑆)) |
31 | 24, 27, 28, 30 | syl21anc 838 |
. . 3
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹 ∈ (∪ 𝑇 ↑m ∪ 𝑆)) |
32 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 = (sigaGen‘𝐾)) |
33 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝜑) |
34 | | ssrab2 3993 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝑇 |
35 | | pwuni 4858 |
. . . . . . . . . . 11
⊢ 𝑇 ⊆ 𝒫 ∪ 𝑇 |
36 | 34, 35 | sstri 3910 |
. . . . . . . . . 10
⊢ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇 |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇) |
38 | | fimacnv 6567 |
. . . . . . . . . . . . 13
⊢ (𝐹:∪
𝑆⟶∪ 𝑇
→ (◡𝐹 “ ∪ 𝑇) = ∪
𝑆) |
39 | 38 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → (◡𝐹 “ ∪ 𝑇) = ∪
𝑆) |
40 | 39, 27 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → (◡𝐹 “ ∪ 𝑇) ∈ 𝑆) |
41 | | imaeq2 5925 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ∪
𝑇 → (◡𝐹 “ 𝑎) = (◡𝐹 “ ∪ 𝑇)) |
42 | 41 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∪
𝑇 → ((◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (◡𝐹 “ ∪ 𝑇) ∈ 𝑆)) |
43 | 42 | elrab 3602 |
. . . . . . . . . . 11
⊢ (∪ 𝑇
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (∪ 𝑇 ∈ 𝑇 ∧ (◡𝐹 “ ∪ 𝑇) ∈ 𝑆)) |
44 | 24, 40, 43 | sylanbrc 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
45 | 6 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑇 ∈ ∪ ran
sigAlgebra) |
46 | 45, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → ∪ 𝑇 ∈ 𝑇) |
47 | | elrabi 3596 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} → 𝑥 ∈ 𝑇) |
48 | 47 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑥 ∈ 𝑇) |
49 | | difelsiga 31813 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 ∈ 𝑇 ∧ 𝑥 ∈ 𝑇) → (∪ 𝑇 ∖ 𝑥) ∈ 𝑇) |
50 | 45, 46, 48, 49 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪
𝑇 ∖ 𝑥) ∈ 𝑇) |
51 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
52 | | ffun 6548 |
. . . . . . . . . . . . . 14
⊢ (𝐹:∪
𝑆⟶∪ 𝑇
→ Fun 𝐹) |
53 | | difpreima 6885 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) = ((◡𝐹 “ ∪ 𝑇) ∖ (◡𝐹 “ 𝑥))) |
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) = ((◡𝐹 “ ∪ 𝑇) ∖ (◡𝐹 “ 𝑥))) |
55 | 39 | difeq1d 4036 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ((◡𝐹 “ ∪ 𝑇) ∖ (◡𝐹 “ 𝑥)) = (∪ 𝑆 ∖ (◡𝐹 “ 𝑥))) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → ((◡𝐹 “ ∪ 𝑇) ∖ (◡𝐹 “ 𝑥)) = (∪ 𝑆 ∖ (◡𝐹 “ 𝑥))) |
57 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑆 ∈ ∪ ran
sigAlgebra) |
58 | 57, 25 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → ∪ 𝑆 ∈ 𝑆) |
59 | | imaeq2 5925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑥 → (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑥)) |
60 | 59 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑥 → ((◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (◡𝐹 “ 𝑥) ∈ 𝑆)) |
61 | 60 | elrab 3602 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝑥 ∈ 𝑇 ∧ (◡𝐹 “ 𝑥) ∈ 𝑆)) |
62 | 61 | simprbi 500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} → (◡𝐹 “ 𝑥) ∈ 𝑆) |
63 | 62 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (◡𝐹 “ 𝑥) ∈ 𝑆) |
64 | | difelsiga 31813 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑆 ∈ 𝑆 ∧ (◡𝐹 “ 𝑥) ∈ 𝑆) → (∪ 𝑆 ∖ (◡𝐹 “ 𝑥)) ∈ 𝑆) |
65 | 57, 58, 63, 64 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪
𝑆 ∖ (◡𝐹 “ 𝑥)) ∈ 𝑆) |
66 | 56, 65 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → ((◡𝐹 “ ∪ 𝑇) ∖ (◡𝐹 “ 𝑥)) ∈ 𝑆) |
67 | 54, 66 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆) |
68 | | imaeq2 5925 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (∪
𝑇 ∖ 𝑥) → (◡𝐹 “ 𝑎) = (◡𝐹 “ (∪ 𝑇 ∖ 𝑥))) |
69 | 68 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (∪
𝑇 ∖ 𝑥) → ((◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆)) |
70 | 69 | elrab 3602 |
. . . . . . . . . . . 12
⊢ ((∪ 𝑇
∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ ((∪
𝑇 ∖ 𝑥) ∈ 𝑇 ∧ (◡𝐹 “ (∪ 𝑇 ∖ 𝑥)) ∈ 𝑆)) |
71 | 50, 67, 70 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (∪
𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
72 | 71 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
73 | 6 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑇 ∈ ∪ ran
sigAlgebra) |
74 | 34 | sspwi 4527 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
{𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 𝑇 |
75 | 74 | sseli 3896 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} → 𝑥 ∈ 𝒫 𝑇) |
76 | 75 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝑇) |
77 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω) |
78 | | sigaclcu 31797 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑇) |
79 | 73, 76, 77, 78 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑇) |
80 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) |
81 | 80 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝐹:∪ 𝑆⟶∪ 𝑇) |
82 | | unipreima 30700 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐹 → (◡𝐹 “ ∪ 𝑥) = ∪ 𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦)) |
83 | 81, 52, 82 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (◡𝐹 “ ∪ 𝑥) = ∪ 𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦)) |
84 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → 𝑆 ∈ ∪ ran
sigAlgebra) |
85 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝐹:∪
𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
86 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝐹:∪
𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
87 | | elelpwi 4525 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → 𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
88 | 85, 86, 87 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝐹:∪
𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
89 | | imaeq2 5925 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑦 → (◡𝐹 “ 𝑎) = (◡𝐹 “ 𝑦)) |
90 | 89 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑦 → ((◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (◡𝐹 “ 𝑦) ∈ 𝑆)) |
91 | 90 | elrab 3602 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝑦 ∈ 𝑇 ∧ (◡𝐹 “ 𝑦) ∈ 𝑆)) |
92 | 91 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} → (◡𝐹 “ 𝑦) ∈ 𝑆) |
93 | 88, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐹:∪
𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) ∧ 𝑦 ∈ 𝑥) → (◡𝐹 “ 𝑦) ∈ 𝑆) |
94 | 93 | ralrimiva 3105 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∀𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦) ∈ 𝑆) |
95 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦𝑥 |
96 | 95 | sigaclcuni 31798 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦) ∈ 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦) ∈ 𝑆) |
97 | 84, 94, 77, 96 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑦 ∈ 𝑥 (◡𝐹 “ 𝑦) ∈ 𝑆) |
98 | 83, 97 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → (◡𝐹 “ ∪ 𝑥) ∈ 𝑆) |
99 | | imaeq2 5925 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = ∪
𝑥 → (◡𝐹 “ 𝑎) = (◡𝐹 “ ∪ 𝑥)) |
100 | 99 | eleq1d 2822 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = ∪
𝑥 → ((◡𝐹 “ 𝑎) ∈ 𝑆 ↔ (◡𝐹 “ ∪ 𝑥) ∈ 𝑆)) |
101 | 100 | elrab 3602 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (∪ 𝑥 ∈ 𝑇 ∧ (◡𝐹 “ ∪ 𝑥) ∈ 𝑆)) |
102 | 79, 98, 101 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
103 | 102 | ex 416 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) ∧ 𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆})) |
104 | 103 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆})) |
105 | 44, 72, 104 | 3jca 1130 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → (∪
𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}))) |
106 | | rabexg 5224 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ∪ ran sigAlgebra → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ V) |
107 | | issiga 31792 |
. . . . . . . . . . 11
⊢ ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ V → ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)
↔ ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇
∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}))))) |
108 | 6, 106, 107 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)
↔ ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇
∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}))))) |
109 | 108 | biimpar 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝒫 ∪ 𝑇
∧ (∪ 𝑇 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (∪ 𝑇 ∖ 𝑥) ∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∧ ∀𝑥 ∈ 𝒫 {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} (𝑥 ≼ ω → ∪ 𝑥
∈ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆})))) → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)) |
110 | 33, 37, 105, 109 | syl12anc 837 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)) |
111 | 3 | unieqd 4833 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑇 =
∪ (sigaGen‘𝐾)) |
112 | | unisg 31823 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ V → ∪ (sigaGen‘𝐾) = ∪ 𝐾) |
113 | 4, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ (sigaGen‘𝐾) = ∪ 𝐾) |
114 | 111, 113 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑇 =
∪ 𝐾) |
115 | 114 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 → (sigAlgebra‘∪ 𝑇) =
(sigAlgebra‘∪ 𝐾)) |
116 | 115 | eleq2d 2823 |
. . . . . . . . 9
⊢ (𝜑 → ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)
↔ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾))) |
117 | 116 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝑇)
↔ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾))) |
118 | 110, 117 | mpbid 235 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾)) |
119 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐾 ⊆ 𝑇) |
120 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆) |
121 | | ssrab 3986 |
. . . . . . . 8
⊢ (𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ (𝐾 ⊆ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) |
122 | 119, 120,
121 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
123 | | sigagenss 31829 |
. . . . . . 7
⊢ (({𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ∈ (sigAlgebra‘∪ 𝐾)
∧ 𝐾 ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) → (sigaGen‘𝐾) ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
124 | 118, 122,
123 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → (sigaGen‘𝐾) ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
125 | 32, 124 | eqsstrd 3939 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 ⊆ {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
126 | 34 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ⊆ 𝑇) |
127 | 125, 126 | eqssd 3918 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 = {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆}) |
128 | | rabid2 3293 |
. . . 4
⊢ (𝑇 = {𝑎 ∈ 𝑇 ∣ (◡𝐹 “ 𝑎) ∈ 𝑆} ↔ ∀𝑎 ∈ 𝑇 (◡𝐹 “ 𝑎) ∈ 𝑆) |
129 | 127, 128 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → ∀𝑎 ∈ 𝑇 (◡𝐹 “ 𝑎) ∈ 𝑆) |
130 | 1 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑆 ∈ ∪ ran
sigAlgebra) |
131 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝑇 ∈ ∪ ran
sigAlgebra) |
132 | 130, 131 | ismbfm 31931 |
. . 3
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑m ∪ 𝑆)
∧ ∀𝑎 ∈
𝑇 (◡𝐹 “ 𝑎) ∈ 𝑆))) |
133 | 31, 129, 132 | mpbir2and 713 |
. 2
⊢ ((𝜑 ∧ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)) → 𝐹 ∈ (𝑆MblFnM𝑇)) |
134 | 21, 133 | impbida 801 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹:∪ 𝑆⟶∪ 𝑇
∧ ∀𝑎 ∈
𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆))) |