Proof of Theorem fsetexb
| Step | Hyp | Ref
| Expression |
| 1 | | ioran 986 |
. . . . . 6
⊢ (¬
((𝐴 ∉ V ∨ 𝐴 = ∅) ∨ 𝐵 ∈ V) ↔ (¬ (𝐴 ∉ V ∨ 𝐴 = ∅) ∧ ¬ 𝐵 ∈ V)) |
| 2 | | df-nel 3047 |
. . . . . . . 8
⊢ (𝐵 ∉ V ↔ ¬ 𝐵 ∈ V) |
| 3 | | ioran 986 |
. . . . . . . . . 10
⊢ (¬
(𝐴 ∉ V ∨ 𝐴 = ∅) ↔ (¬ 𝐴 ∉ V ∧ ¬ 𝐴 = ∅)) |
| 4 | | nnel 3056 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∉ V ↔ 𝐴 ∈ V) |
| 5 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
| 6 | 5 | bicomi 224 |
. . . . . . . . . . 11
⊢ (¬
𝐴 = ∅ ↔ 𝐴 ≠ ∅) |
| 7 | 4, 6 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∉ V ∧ ¬
𝐴 = ∅) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅)) |
| 8 | 3, 7 | bitri 275 |
. . . . . . . . 9
⊢ (¬
(𝐴 ∉ V ∨ 𝐴 = ∅) ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅)) |
| 9 | | fsetprcnex 8902 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) |
| 10 | 9 | ex 412 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐴 ≠ ∅) → (𝐵 ∉ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)) |
| 11 | 8, 10 | sylbi 217 |
. . . . . . . 8
⊢ (¬
(𝐴 ∉ V ∨ 𝐴 = ∅) → (𝐵 ∉ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)) |
| 12 | 2, 11 | biimtrrid 243 |
. . . . . . 7
⊢ (¬
(𝐴 ∉ V ∨ 𝐴 = ∅) → (¬ 𝐵 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)) |
| 13 | 12 | imp 406 |
. . . . . 6
⊢ ((¬
(𝐴 ∉ V ∨ 𝐴 = ∅) ∧ ¬ 𝐵 ∈ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) |
| 14 | 1, 13 | sylbi 217 |
. . . . 5
⊢ (¬
((𝐴 ∉ V ∨ 𝐴 = ∅) ∨ 𝐵 ∈ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) |
| 15 | | df-nel 3047 |
. . . . 5
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V ↔ ¬ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 16 | 14, 15 | sylib 218 |
. . . 4
⊢ (¬
((𝐴 ∉ V ∨ 𝐴 = ∅) ∨ 𝐵 ∈ V) → ¬ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 17 | 16 | con4i 114 |
. . 3
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V → ((𝐴 ∉ V ∨ 𝐴 = ∅) ∨ 𝐵 ∈ V)) |
| 18 | | df-3or 1088 |
. . 3
⊢ ((𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V) ↔ ((𝐴 ∉ V ∨ 𝐴 = ∅) ∨ 𝐵 ∈ V)) |
| 19 | 17, 18 | sylibr 234 |
. 2
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V → (𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V)) |
| 20 | | fsetdmprc0 8895 |
. . . 4
⊢ (𝐴 ∉ V → {𝑓 ∣ 𝑓 Fn 𝐴} = ∅) |
| 21 | | ffn 6736 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
| 22 | 21 | ss2abi 4067 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ⊆ {𝑓 ∣ 𝑓 Fn 𝐴} |
| 23 | | sseq0 4403 |
. . . . . 6
⊢ (({𝑓 ∣ 𝑓:𝐴⟶𝐵} ⊆ {𝑓 ∣ 𝑓 Fn 𝐴} ∧ {𝑓 ∣ 𝑓 Fn 𝐴} = ∅) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅) |
| 24 | 22, 23 | mpan 690 |
. . . . 5
⊢ ({𝑓 ∣ 𝑓 Fn 𝐴} = ∅ → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅) |
| 25 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 26 | 24, 25 | eqeltrdi 2849 |
. . . 4
⊢ ({𝑓 ∣ 𝑓 Fn 𝐴} = ∅ → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 27 | 20, 26 | syl 17 |
. . 3
⊢ (𝐴 ∉ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 28 | | feq2 6717 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑓:𝐴⟶𝐵 ↔ 𝑓:∅⟶𝐵)) |
| 29 | 28 | abbidv 2808 |
. . . . 5
⊢ (𝐴 = ∅ → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = {𝑓 ∣ 𝑓:∅⟶𝐵}) |
| 30 | | fset0 8894 |
. . . . 5
⊢ {𝑓 ∣ 𝑓:∅⟶𝐵} = {∅} |
| 31 | 29, 30 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = ∅ → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = {∅}) |
| 32 | | p0ex 5384 |
. . . 4
⊢ {∅}
∈ V |
| 33 | 31, 32 | eqeltrdi 2849 |
. . 3
⊢ (𝐴 = ∅ → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 34 | | fsetex 8896 |
. . 3
⊢ (𝐵 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 35 | 27, 33, 34 | 3jaoi 1430 |
. 2
⊢ ((𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
| 36 | 19, 35 | impbii 209 |
1
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V ↔ (𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V)) |