Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . 6
⊢ 𝑦 ∈ V |
2 | 1 | brdom 7967 |
. . . . 5
⊢ (𝐴 ≼ 𝑦 ↔ ∃𝑓 𝑓:𝐴–1-1→𝑦) |
3 | | f1f 6101 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴⟶𝑦) |
4 | | frn 6053 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴⟶𝑦 → ran 𝑓 ⊆ 𝑦) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–1-1→𝑦 → ran 𝑓 ⊆ 𝑦) |
6 | | onss 6990 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → 𝑦 ⊆ On) |
7 | | sstr2 3610 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ⊆ 𝑦 → (𝑦 ⊆ On → ran 𝑓 ⊆ On)) |
8 | 5, 6, 7 | syl2im 40 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → ran 𝑓 ⊆ On)) |
9 | | epweon 6983 |
. . . . . . . . . 10
⊢ E We
On |
10 | | wess 5101 |
. . . . . . . . . 10
⊢ (ran
𝑓 ⊆ On → ( E We
On → E We ran 𝑓)) |
11 | 8, 9, 10 | syl6mpi 67 |
. . . . . . . . 9
⊢ (𝑓:𝐴–1-1→𝑦 → (𝑦 ∈ On → E We ran 𝑓)) |
12 | 11 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → E We ran 𝑓)) |
13 | | f1f1orn 6148 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–1-1→𝑦 → 𝑓:𝐴–1-1-onto→ran
𝑓) |
14 | | eqid 2622 |
. . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} = {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} |
15 | 14 | f1owe 6603 |
. . . . . . . . . 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 5186 |
. . . . . . . . . 10
⊢
({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 ↔ ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴) |
18 | | reldom 7961 |
. . . . . . . . . . . 12
⊢ Rel
≼ |
19 | 18 | brrelexi 5158 |
. . . . . . . . . . 11
⊢ (𝐴 ≼ 𝑦 → 𝐴 ∈ V) |
20 | | sqxpexg 6963 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 × 𝐴) ∈ V) |
21 | | incom 3805 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐴) ∩ {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) = ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) |
22 | | inex1g 4801 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ {〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)}) ∈ V) |
23 | 21, 22 | syl5eqelr 2706 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐴) ∈ V → ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V) |
24 | | weeq1 5102 |
. . . . . . . . . . . 12
⊢ (𝑥 = ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) → (𝑥 We 𝐴 ↔ ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴)) |
25 | 24 | spcegv 3294 |
. . . . . . . . . . 11
⊢
(({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) ∈ V → (({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
26 | 19, 20, 23, 25 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝐴 ≼ 𝑦 → (({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
27 | 17, 26 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐴 ≼ 𝑦 → ({〈𝑤, 𝑧〉 ∣ (𝑓‘𝑤) E (𝑓‘𝑧)} We 𝐴 → ∃𝑥 𝑥 We 𝐴)) |
28 | 16, 27 | sylan9r 690 |
. . . . . . . 8
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → ( E We ran 𝑓 → ∃𝑥 𝑥 We 𝐴)) |
29 | 12, 28 | syld 47 |
. . . . . . 7
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑓:𝐴–1-1→𝑦) → (𝑦 ∈ On → ∃𝑥 𝑥 We 𝐴)) |
30 | 29 | impancom 456 |
. . . . . 6
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴)) |
31 | 30 | exlimdv 1861 |
. . . . 5
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (∃𝑓 𝑓:𝐴–1-1→𝑦 → ∃𝑥 𝑥 We 𝐴)) |
32 | 2, 31 | syl5bi 232 |
. . . 4
⊢ ((𝐴 ≼ 𝑦 ∧ 𝑦 ∈ On) → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)) |
33 | 32 | ex 450 |
. . 3
⊢ (𝐴 ≼ 𝑦 → (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴))) |
34 | 33 | pm2.43b 55 |
. 2
⊢ (𝑦 ∈ On → (𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)) |
35 | 34 | rexlimiv 3027 |
1
⊢
(∃𝑦 ∈ On
𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴) |