Step | Hyp | Ref
| Expression |
1 | | fssxp 6701 |
. . . . . . . . 9
⊢ (𝑓:𝑥⟶{1o, 2o} →
𝑓 ⊆ (𝑥 × {1o,
2o})) |
2 | 1 | adantl 483 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ⊆ (𝑥 × {1o,
2o})) |
3 | | onss 7724 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
4 | 3 | adantr 482 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑥 ⊆
On) |
5 | | xpss1 5657 |
. . . . . . . . 9
⊢ (𝑥 ⊆ On → (𝑥 × {1o,
2o}) ⊆ (On × {1o,
2o})) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ (𝑥 ×
{1o, 2o}) ⊆ (On × {1o,
2o})) |
7 | 2, 6 | sstrd 3959 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ⊆ (On
× {1o, 2o})) |
8 | | velpw 4570 |
. . . . . . 7
⊢ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ↔ 𝑓 ⊆ (On × {1o,
2o})) |
9 | 7, 8 | sylibr 233 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ∈ 𝒫
(On × {1o, 2o})) |
10 | | ffun 6676 |
. . . . . . 7
⊢ (𝑓:𝑥⟶{1o, 2o} →
Fun 𝑓) |
11 | 10 | adantl 483 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ Fun 𝑓) |
12 | | fdm 6682 |
. . . . . . . 8
⊢ (𝑓:𝑥⟶{1o, 2o} →
dom 𝑓 = 𝑥) |
13 | 12 | adantl 483 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ dom 𝑓 = 𝑥) |
14 | | simpl 484 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑥 ∈
On) |
15 | 13, 14 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ dom 𝑓 ∈
On) |
16 | 9, 11, 15 | jca32 517 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ (𝑓 ∈ 𝒫
(On × {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
17 | 16 | rexlimiva 3145 |
. . . 4
⊢
(∃𝑥 ∈ On
𝑓:𝑥⟶{1o, 2o} →
(𝑓 ∈ 𝒫 (On
× {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
18 | | simprr 772 |
. . . . 5
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → dom 𝑓 ∈ On) |
19 | | feq2 6655 |
. . . . . 6
⊢ (𝑥 = dom 𝑓 → (𝑓:𝑥⟶{1o, 2o} ↔
𝑓:dom 𝑓⟶{1o,
2o})) |
20 | 19 | adantl 483 |
. . . . 5
⊢ (((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) ∧ 𝑥 = dom 𝑓) → (𝑓:𝑥⟶{1o, 2o} ↔
𝑓:dom 𝑓⟶{1o,
2o})) |
21 | | simpl 484 |
. . . . . 6
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On) → Fun 𝑓) |
22 | | elpwi 4572 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) → 𝑓 ⊆ (On × {1o,
2o})) |
23 | | funssxp 6702 |
. . . . . . 7
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ (On × {1o,
2o})) ↔ (𝑓:dom 𝑓⟶{1o, 2o} ∧
dom 𝑓 ⊆
On)) |
24 | 23 | simplbi 499 |
. . . . . 6
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ (On × {1o,
2o})) → 𝑓:dom 𝑓⟶{1o,
2o}) |
25 | 21, 22, 24 | syl2anr 598 |
. . . . 5
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → 𝑓:dom 𝑓⟶{1o,
2o}) |
26 | 18, 20, 25 | rspcedvd 3586 |
. . . 4
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → ∃𝑥 ∈ On 𝑓:𝑥⟶{1o,
2o}) |
27 | 17, 26 | impbii 208 |
. . 3
⊢
(∃𝑥 ∈ On
𝑓:𝑥⟶{1o, 2o} ↔
(𝑓 ∈ 𝒫 (On
× {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
28 | 27 | abbii 2807 |
. 2
⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o, 2o}} =
{𝑓 ∣ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))} |
29 | | df-no 27007 |
. 2
⊢ No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o,
2o}} |
30 | | df-rab 3411 |
. 2
⊢ {𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)} = {𝑓 ∣ (𝑓 ∈ 𝒫 (On × {1o,
2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))} |
31 | 28, 29, 30 | 3eqtr4i 2775 |
1
⊢ No = {𝑓 ∈ 𝒫 (On × {1o,
2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)} |