Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
2 | 1 | brdom 7853 |
. . . . 5
⊢ (𝐴 ≼ 𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1→𝑦) |
3 | | f1f 6014 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴⟶𝑦) |
4 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴⟶𝑦 → ran 𝑓 ⊆ 𝑦) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1→𝑦 → ran 𝑓 ⊆ 𝑦) |
6 | | onss 6882 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → 𝑦 ⊆ On) |
7 | | sstr2 3575 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ⊆ 𝑦 → (𝑦 ⊆ On → ran 𝑓 ⊆ On)) |
8 | 5, 6, 7 | syl2im 39 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → ran 𝑓 ⊆ On)) |
9 | | epweon 6875 |
. . . . . . . . . 10
⊢ E We
On |
10 | | wess 5025 |
. . . . . . . . . 10
⊢ (ran
𝑓 ⊆ On → ( E We
On → E We ran 𝑓)) |
11 | 8, 9, 10 | syl6mpi 65 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → E We ran 𝑓)) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → E We ran 𝑓)) |
13 | | f1f1orn 6061 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴–1-1-onto→ran
𝑓) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} = {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} |
15 | 14 | f1owe 6503 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1-onto→ran
𝑓 → ( E We ran 𝑓 → {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴)) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝑦 → ( E We ran 𝑓 → {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴)) |
17 | | weinxp 5109 |
. . . . . . . . . 10
⊢
({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 ↔ ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴) |
18 | | reldom 7847 |
. . . . . . . . . . . 12
⊢ Rel
≼ |
19 | 18 | brrelexi 5082 |
. . . . . . . . . . 11
⊢ (𝐴 ≼ 𝑦 → 𝐴 ∈ V) |
20 | | sqxpexg 6861 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 × 𝐴) ∈ V) |
21 | | incom 3767 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐴) ∩ {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) = ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) |
22 | | inex1g 4729 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) ∈ V) |
23 | 21, 22 | syl5eqelr 2693 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐴) ∈ V → ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V) |
24 | | weeq1 5026 |
. . . . . . . . . . . 12
⊢ (𝑥 = ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) → (𝑥 We 𝐴 ↔ ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
25 | 24 | spcegv 3267 |
. . . . . . . . . . 11
⊢
(({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V → (({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
26 | 19, 20, 23, 25 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝐴 ≼ 𝑦 → (({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
27 | 17, 26 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝐴 ≼ 𝑦 → ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
28 | 16, 27 | sylan9r 688 |
. . . . . . . 8
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → ( E We ran 𝑓 → ∃𝑥 𝑥 We 𝐴)) |
29 | 12, 28 | syld 46 |
. . . . . . 7
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → ∃𝑥 𝑥 We 𝐴)) |
30 | 29 | impancom 455 |
. . . . . 6
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴)) |
31 | 30 | exlimdv 1848 |
. . . . 5
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (∃𝑓 𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴)) |
32 | 2, 31 | syl5bi 231 |
. . . 4
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)) |
33 | 32 | ex 449 |
. . 3
⊢ (𝐴 ≼ 𝑦 → (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴))) |
34 | 33 | pm2.43b 53 |
. 2
⊢ (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)) |
35 | 34 | rexlimiv 3009 |
1
⊢
(∃𝑦 ∈ On
𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴) |