Proof of Theorem bnj149
Step | Hyp | Ref
| Expression |
1 | | simpr1 1060 |
. . . . . . . 8
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → 𝑓 Fn 1𝑜) |
2 | | df1o2 7459 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
3 | 2 | fneq2i 5900 |
. . . . . . . 8
⊢ (𝑓 Fn 1𝑜 ↔
𝑓 Fn
{∅}) |
4 | 1, 3 | sylib 207 |
. . . . . . 7
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → 𝑓 Fn {∅}) |
5 | | simpr2 1061 |
. . . . . . . . . 10
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → 𝜑′) |
6 | | bnj149.6 |
. . . . . . . . . 10
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
7 | 5, 6 | sylib 207 |
. . . . . . . . 9
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
8 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑓‘∅) ∈
V |
9 | 8 | elsn 4140 |
. . . . . . . . 9
⊢ ((𝑓‘∅) ∈ {
pred(𝑥, 𝐴, 𝑅)} ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
10 | 7, 9 | sylibr 223 |
. . . . . . . 8
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → (𝑓‘∅) ∈ { pred(𝑥, 𝐴, 𝑅)}) |
11 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → (𝑓‘𝑔) = (𝑓‘∅)) |
13 | 12 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → ((𝑓‘𝑔) ∈ { pred(𝑥, 𝐴, 𝑅)} ↔ (𝑓‘∅) ∈ { pred(𝑥, 𝐴, 𝑅)})) |
14 | 11, 13 | ralsn 4169 |
. . . . . . . 8
⊢
(∀𝑔 ∈
{∅} (𝑓‘𝑔) ∈ { pred(𝑥, 𝐴, 𝑅)} ↔ (𝑓‘∅) ∈ { pred(𝑥, 𝐴, 𝑅)}) |
15 | 10, 14 | sylibr 223 |
. . . . . . 7
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → ∀𝑔 ∈ {∅} (𝑓‘𝑔) ∈ { pred(𝑥, 𝐴, 𝑅)}) |
16 | | ffnfv 6295 |
. . . . . . 7
⊢ (𝑓:{∅}⟶{ pred(𝑥, 𝐴, 𝑅)} ↔ (𝑓 Fn {∅} ∧ ∀𝑔 ∈ {∅} (𝑓‘𝑔) ∈ { pred(𝑥, 𝐴, 𝑅)})) |
17 | 4, 15, 16 | sylanbrc 695 |
. . . . . 6
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → 𝑓:{∅}⟶{ pred(𝑥, 𝐴, 𝑅)}) |
18 | | bnj93 30187 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → pred(𝑥, 𝐴, 𝑅) ∈ V) |
20 | | fsng 6310 |
. . . . . . 7
⊢ ((∅
∈ V ∧ pred(𝑥,
𝐴, 𝑅) ∈ V) → (𝑓:{∅}⟶{ pred(𝑥, 𝐴, 𝑅)} ↔ 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉})) |
21 | 11, 19, 20 | sylancr 694 |
. . . . . 6
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → (𝑓:{∅}⟶{ pred(𝑥, 𝐴, 𝑅)} ↔ 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉})) |
22 | 17, 21 | mpbid 221 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) → 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉}) |
23 | 22 | ex 449 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′) → 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉})) |
24 | 23 | alrimiv 1842 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∀𝑓((𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′) → 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉})) |
25 | | mo2icl 3352 |
. . 3
⊢
(∀𝑓((𝑓 Fn 1𝑜 ∧
𝜑′ ∧ 𝜓′) → 𝑓 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉}) → ∃*𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) |
26 | 24, 25 | syl 17 |
. 2
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) |
27 | | bnj149.1 |
. 2
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))) |
28 | 26, 27 | mpbir 220 |
1
⊢ 𝜃1 |