| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simplll 774 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII) | 
| 2 |  | ssrab2 4079 | . . . . . . . . . . . . . . . . . . 19
⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 | 
| 3 |  | sstr 3991 | . . . . . . . . . . . . . . . . . . 19
⊢ (({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) | 
| 4 | 2, 3 | mpan 690 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ⊆ 𝐴 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) | 
| 5 |  | elpw2g 5332 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ FinII →
({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)) | 
| 6 | 5 | biimpar 477 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ FinII ∧
{𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴) | 
| 7 | 4, 6 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ FinII ∧
𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴) | 
| 8 | 7 | ralrimivw 3149 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ FinII ∧
𝑥 ⊆ 𝐴) → ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴) | 
| 9 |  | vex 3483 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V | 
| 10 | 9 | rabex 5338 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V | 
| 11 | 10 | rgenw 3064 | . . . . . . . . . . . . . . . . 17
⊢
∀𝑣 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V | 
| 12 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) | 
| 13 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)) | 
| 14 | 12, 13 | ralrnmptw 7113 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑣 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)) | 
| 15 | 11, 14 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴) | 
| 16 | 8, 15 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ FinII ∧
𝑥 ⊆ 𝐴) → ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴) | 
| 17 |  | dfss3 3971 | . . . . . . . . . . . . . . 15
⊢ (ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴) | 
| 18 | 16, 17 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ FinII ∧
𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) | 
| 19 | 18 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) | 
| 21 | 10, 12 | dmmpti 6711 | . . . . . . . . . . . . . . 15
⊢ dom
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = 𝑥 | 
| 22 | 21 | neeq1i 3004 | . . . . . . . . . . . . . 14
⊢ (dom
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅) | 
| 23 |  | dm0rn0 5934 | . . . . . . . . . . . . . . 15
⊢ (dom
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅) | 
| 24 | 23 | necon3bii 2992 | . . . . . . . . . . . . . 14
⊢ (dom
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅) | 
| 25 | 22, 24 | sylbb1 237 | . . . . . . . . . . . . 13
⊢ (𝑥 ≠ ∅ → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅) | 
| 26 | 25 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅) | 
| 27 |  | soss 5611 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or 𝑥)) | 
| 28 | 27 | impcom 407 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → 𝑅 Or 𝑥) | 
| 29 |  | porpss 7748 | . . . . . . . . . . . . . . . . 17
⊢ 
[⊊] Po ran (𝑣
∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 Or 𝑥 → [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 31 |  | solin 5618 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣)) | 
| 32 |  | fin2solem 37614 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 33 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 𝑦 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑦)) | 
| 34 | 33 | rabbidv 3443 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 36 |  | fin2solem 37614 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 37 | 36 | ancom2s 650 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 38 | 32, 35, 37 | 3orim123d 1445 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ((𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) | 
| 39 | 31, 38 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 40 | 39 | ralrimivva 3201 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 Or 𝑥 → ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 41 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 42 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 43 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 44 | 41, 42, 43 | 3orbi123d 1436 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ((𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) | 
| 45 | 44 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) | 
| 46 | 12, 45 | ralrnmptw 7113 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑣 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) | 
| 47 | 11, 46 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑢 ∈
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 48 | 40, 47 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)) | 
| 49 | 48 | r19.21bi 3250 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)) | 
| 50 | 9 | rabex 5338 | . . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V | 
| 51 | 50 | rgenw 3064 | . . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑦 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V | 
| 52 | 34 | cbvmptv 5254 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑦 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) | 
| 53 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 54 |  | eqeq2 2748 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 = 𝑧 ↔ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 55 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)) | 
| 56 | 53, 54, 55 | 3orbi123d 1436 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))) | 
| 57 | 52, 56 | ralrnmptw 7113 | . . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑦 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))) | 
| 58 | 51, 57 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑧 ∈
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)) | 
| 59 | 49, 58 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢)) | 
| 60 | 59 | r19.21bi 3250 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢)) | 
| 61 | 60 | anasss 466 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢)) | 
| 62 | 30, 61 | issod 5626 | . . . . . . . . . . . . . . 15
⊢ (𝑅 Or 𝑥 → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 63 | 28, 62 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 64 | 63 | adantll 714 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → [⊊] Or
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 66 |  | fin2i2 10359 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ FinII ∧
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ∧ [⊊] Or
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 67 | 1, 20, 26, 65, 66 | syl22anc 838 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 68 | 52, 50 | elrnmpti 5972 | . . . . . . . . . . 11
⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) | 
| 69 | 67, 68 | sylib 218 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) | 
| 70 |  | ssel2 3977 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴) | 
| 71 |  | sonr 5615 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 Or 𝐴 ∧ 𝑧 ∈ 𝐴) → ¬ 𝑧𝑅𝑧) | 
| 72 | 70, 71 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥)) → ¬ 𝑧𝑅𝑧) | 
| 73 | 72 | anassrs 467 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧) | 
| 74 | 73 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧) | 
| 76 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑦 ↔ 𝑧𝑅𝑦)) | 
| 77 | 76 | elrab 3691 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑦)) | 
| 78 | 77 | simplbi2 500 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑥 → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 79 | 78 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 80 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V | 
| 81 | 80 | elint2 4952 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦) | 
| 82 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 83 | 12, 82 | ralrnmptw 7113 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑣 ∈
𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) | 
| 84 | 11, 83 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) | 
| 85 | 81, 84 | bitri 275 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) | 
| 86 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 𝑧 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑧)) | 
| 87 | 86 | rabbidv 3443 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}) | 
| 88 | 87 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 𝑧 → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | 
| 89 | 88 | rspcv 3617 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | 
| 90 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑧 ↔ 𝑧𝑅𝑧)) | 
| 91 | 90 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑧)) | 
| 92 | 91 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} → 𝑧𝑅𝑧) | 
| 93 | 89, 92 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧)) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧)) | 
| 95 | 85, 94 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (𝑧 ∈ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧)) | 
| 96 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})) | 
| 97 | 96 | imbi1d 341 | . . . . . . . . . . . . . . . . . . . 20
⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑧 ∈ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧))) | 
| 98 | 95, 97 | syl5ibcom 245 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧))) | 
| 99 | 98 | imp 406 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)) | 
| 100 | 79, 99 | syld 47 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧)) | 
| 101 | 100 | adantlll 718 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧)) | 
| 102 | 75, 101 | mtod 198 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦) | 
| 103 | 102 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → (∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦)) | 
| 104 | 103 | ralrimdva 3153 | . . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) → (∩ ran
(𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 105 | 104 | reximdva 3167 | . . . . . . . . . . . 12
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 106 | 105 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 107 | 106 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 108 | 69, 107 | mpd 15 | . . . . . . . . 9
⊢ ((((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) | 
| 109 | 108 | expl 457 | . . . . . . . 8
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 110 | 109 | alrimiv 1926 | . . . . . . 7
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 111 |  | df-fr 5636 | . . . . . . 7
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | 
| 112 | 110, 111 | sylibr 234 | . . . . . 6
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → 𝑅 Fr 𝐴) | 
| 113 |  | simpr 484 | . . . . . 6
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → 𝑅 Or 𝐴) | 
| 114 |  | df-we 5638 | . . . . . 6
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | 
| 115 | 112, 113,
114 | sylanbrc 583 | . . . . 5
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → 𝑅 We 𝐴) | 
| 116 |  | weinxp 5769 | . . . . 5
⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) | 
| 117 | 115, 116 | sylib 218 | . . . 4
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) | 
| 118 |  | sqxpexg 7776 | . . . . . 6
⊢ (𝐴 ∈ FinII →
(𝐴 × 𝐴) ∈ V) | 
| 119 |  | incom 4208 | . . . . . . 7
⊢ (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅) | 
| 120 |  | inex1g 5318 | . . . . . . 7
⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V) | 
| 121 | 119, 120 | eqeltrid 2844 | . . . . . 6
⊢ ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) | 
| 122 |  | weeq1 5671 | . . . . . . 7
⊢ (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)) | 
| 123 | 122 | spcegv 3596 | . . . . . 6
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴)) | 
| 124 | 118, 121,
123 | 3syl 18 | . . . . 5
⊢ (𝐴 ∈ FinII →
((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴)) | 
| 125 | 124 | imp 406 | . . . 4
⊢ ((𝐴 ∈ FinII ∧
(𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴) | 
| 126 | 117, 125 | syldan 591 | . . 3
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴) | 
| 127 |  | ween 10076 | . . 3
⊢ (𝐴 ∈ dom card ↔
∃𝑧 𝑧 We 𝐴) | 
| 128 | 126, 127 | sylibr 234 | . 2
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → 𝐴 ∈ dom card) | 
| 129 |  | fin23 10430 | . . . . 5
⊢ (𝐴 ∈ FinII →
𝐴 ∈
FinIII) | 
| 130 |  | fin34 10431 | . . . . 5
⊢ (𝐴 ∈ FinIII →
𝐴 ∈
FinIV) | 
| 131 |  | fin45 10433 | . . . . 5
⊢ (𝐴 ∈ FinIV →
𝐴 ∈
FinV) | 
| 132 | 129, 130,
131 | 3syl 18 | . . . 4
⊢ (𝐴 ∈ FinII →
𝐴 ∈
FinV) | 
| 133 |  | fin56 10434 | . . . 4
⊢ (𝐴 ∈ FinV →
𝐴 ∈
FinVI) | 
| 134 |  | fin67 10436 | . . . 4
⊢ (𝐴 ∈ FinVI →
𝐴 ∈
FinVII) | 
| 135 | 132, 133,
134 | 3syl 18 | . . 3
⊢ (𝐴 ∈ FinII →
𝐴 ∈
FinVII) | 
| 136 |  | fin71num 10438 | . . . 4
⊢ (𝐴 ∈ dom card → (𝐴 ∈ FinVII ↔
𝐴 ∈
Fin)) | 
| 137 | 136 | biimpac 478 | . . 3
⊢ ((𝐴 ∈ FinVII ∧
𝐴 ∈ dom card) →
𝐴 ∈
Fin) | 
| 138 | 135, 137 | sylan 580 | . 2
⊢ ((𝐴 ∈ FinII ∧
𝐴 ∈ dom card) →
𝐴 ∈
Fin) | 
| 139 | 128, 138 | syldan 591 | 1
⊢ ((𝐴 ∈ FinII ∧
𝑅 Or 𝐴) → 𝐴 ∈ Fin) |