| Step | Hyp | Ref
| Expression |
| 1 | | fssxp 6763 |
. . . . . . . . 9
⊢ (𝑓:𝑥⟶{1o, 2o} →
𝑓 ⊆ (𝑥 × {1o,
2o})) |
| 2 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ⊆ (𝑥 × {1o,
2o})) |
| 3 | | onss 7805 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
| 4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑥 ⊆
On) |
| 5 | | xpss1 5704 |
. . . . . . . . 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 3994 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ⊆ (On
× {1o, 2o})) |
| 8 | | velpw 4605 |
. . . . . . 7
⊢ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ↔ 𝑓 ⊆ (On × {1o,
2o})) |
| 9 | 7, 8 | sylibr 234 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑓 ∈ 𝒫
(On × {1o, 2o})) |
| 10 | | ffun 6739 |
. . . . . . 7
⊢ (𝑓:𝑥⟶{1o, 2o} →
Fun 𝑓) |
| 11 | 10 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ Fun 𝑓) |
| 12 | | fdm 6745 |
. . . . . . . 8
⊢ (𝑓:𝑥⟶{1o, 2o} →
dom 𝑓 = 𝑥) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ dom 𝑓 = 𝑥) |
| 14 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ 𝑥 ∈
On) |
| 15 | 13, 14 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ dom 𝑓 ∈
On) |
| 16 | 9, 11, 15 | jca32 515 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑓:𝑥⟶{1o, 2o})
→ (𝑓 ∈ 𝒫
(On × {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
| 17 | 16 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑥 ∈ On
𝑓:𝑥⟶{1o, 2o} →
(𝑓 ∈ 𝒫 (On
× {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
| 18 | | simprr 773 |
. . . . 5
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → dom 𝑓 ∈ On) |
| 19 | | feq2 6717 |
. . . . . 6
⊢ (𝑥 = dom 𝑓 → (𝑓:𝑥⟶{1o, 2o} ↔
𝑓:dom 𝑓⟶{1o,
2o})) |
| 20 | 19 | adantl 481 |
. . . . 5
⊢ (((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) ∧ 𝑥 = dom 𝑓) → (𝑓:𝑥⟶{1o, 2o} ↔
𝑓:dom 𝑓⟶{1o,
2o})) |
| 21 | | simpl 482 |
. . . . . 6
⊢ ((Fun
𝑓 ∧ dom 𝑓 ∈ On) → Fun 𝑓) |
| 22 | | elpwi 4607 |
. . . . . 6
⊢ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) → 𝑓 ⊆ (On × {1o,
2o})) |
| 23 | | funssxp 6764 |
. . . . . . 7
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ (On × {1o,
2o})) ↔ (𝑓:dom 𝑓⟶{1o, 2o} ∧
dom 𝑓 ⊆
On)) |
| 24 | 23 | simplbi 497 |
. . . . . 6
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ (On × {1o,
2o})) → 𝑓:dom 𝑓⟶{1o,
2o}) |
| 25 | 21, 22, 24 | syl2anr 597 |
. . . . 5
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → 𝑓:dom 𝑓⟶{1o,
2o}) |
| 26 | 18, 20, 25 | rspcedvd 3624 |
. . . 4
⊢ ((𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) → ∃𝑥 ∈ On 𝑓:𝑥⟶{1o,
2o}) |
| 27 | 17, 26 | impbii 209 |
. . 3
⊢
(∃𝑥 ∈ On
𝑓:𝑥⟶{1o, 2o} ↔
(𝑓 ∈ 𝒫 (On
× {1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))) |
| 28 | 27 | abbii 2809 |
. 2
⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o, 2o}} =
{𝑓 ∣ (𝑓 ∈ 𝒫 (On ×
{1o, 2o}) ∧ (Fun 𝑓 ∧ dom 𝑓 ∈ On))} |
| 29 | | df-no 27687 |
. 2
⊢ No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o,
2o}} |
| 30 | | df-rab 3437 |
. 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)} |