Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fin2so Structured version   Visualization version   GIF version

Theorem fin2so 33063
Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)
Assertion
Ref Expression
fin2so ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Proof of Theorem fin2so
Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplll 797 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2 ssrab2 3671 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥
3 sstr 3595 . . . . . . . . . . . . . . . . . . 19 (({𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
42, 3mpan 705 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
5 elpw2g 4792 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ FinII → ({𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴))
65biimpar 502 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ FinII ∧ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
74, 6sylan2 491 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ FinII𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
87ralrimivw 2962 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9 vex 3192 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
109rabex 4778 . . . . . . . . . . . . . . . . . 18 {𝑤𝑥𝑤𝑅𝑣} ∈ V
1110rgenw 2919 . . . . . . . . . . . . . . . . 17 𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V
12 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
13 eleq1 2686 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1412, 13ralrnmpt 6329 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1511, 14ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
168, 15sylibr 224 . . . . . . . . . . . . . . 15 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17 dfss3 3577 . . . . . . . . . . . . . . 15 (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
1816, 17sylibr 224 . . . . . . . . . . . . . 14 ((𝐴 ∈ FinII𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
1918adantlr 750 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2019adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2110, 12dmmpti 5985 . . . . . . . . . . . . . . 15 dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = 𝑥
2221neeq1i 2854 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23 dm0rn0 5307 . . . . . . . . . . . . . . 15 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅)
2423necon3bii 2842 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2522, 24sylbb1 227 . . . . . . . . . . . . 13 (𝑥 ≠ ∅ → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2625adantl 482 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
27 soss 5018 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝑥))
2827impcom 446 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝑥𝐴) → 𝑅 Or 𝑥)
29 porpss 6901 . . . . . . . . . . . . . . . . 17 [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
3029a1i 11 . . . . . . . . . . . . . . . 16 (𝑅 Or 𝑥 → [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
31 solin 5023 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣))
32 fin2solem 33062 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦 → {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
33 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑦 → (𝑤𝑅𝑣𝑤𝑅𝑦))
3433rabbidv 3180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦})
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
36 fin2solem 33062 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑣𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3736ancom2s 843 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3832, 35, 373orim123d 1404 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ((𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
3931, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4039ralrimivva 2966 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Or 𝑥 → ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
41 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
42 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 = {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
43 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ({𝑤𝑥𝑤𝑅𝑦} [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4441, 42, 433orbi123d 1395 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ((𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4544ralbidv 2981 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4612, 45ralrnmpt 6329 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4711, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4840, 47sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
4948r19.21bi 2927 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
509rabex 4778 . . . . . . . . . . . . . . . . . . . . 21 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5150rgenw 2919 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5234cbvmptv 4715 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑦𝑥 ↦ {𝑤𝑥𝑤𝑅𝑦})
53 breq2 4622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 [] 𝑧𝑢 [] {𝑤𝑥𝑤𝑅𝑦}))
54 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 = 𝑧𝑢 = {𝑤𝑥𝑤𝑅𝑦}))
55 breq1 4621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5653, 54, 553orbi123d 1395 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → ((𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5752, 56ralrnmpt 6329 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5851, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5949, 58sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6059r19.21bi 2927 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6160anasss 678 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6230, 61issod 5030 . . . . . . . . . . . . . . 15 (𝑅 Or 𝑥 → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6328, 62syl 17 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6463adantll 749 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6564adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
66 fin2i2 9092 . . . . . . . . . . . 12 (((𝐴 ∈ FinII ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ∧ [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
671, 20, 26, 65, 66syl22anc 1324 . . . . . . . . . . 11 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6852, 50elrnmpti 5341 . . . . . . . . . . 11 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
6967, 68sylib 208 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
70 ssel2 3582 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧𝑥) → 𝑧𝐴)
71 sonr 5021 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴𝑧𝐴) → ¬ 𝑧𝑅𝑧)
7270, 71sylan2 491 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑧𝑥)) → ¬ 𝑧𝑅𝑧)
7372anassrs 679 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7473adantlr 750 . . . . . . . . . . . . . . . . 17 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7574adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76 breq1 4621 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑤𝑅𝑦𝑧𝑅𝑦))
7776elrab 3350 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} ↔ (𝑧𝑥𝑧𝑅𝑦))
7877simplbi2 654 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
7978ad2antlr 762 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
80 vex 3192 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
8180elint2 4452 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦)
82 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑧𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8312, 82ralrnmpt 6329 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8411, 83ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
8581, 84bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
86 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑧 → (𝑤𝑅𝑣𝑤𝑅𝑧))
8786rabbidv 3180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑧})
8887eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
8988rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
90 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑅𝑧𝑧𝑅𝑧))
9190elrab 3350 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} ↔ (𝑧𝑥𝑧𝑅𝑧))
9291simprbi 480 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} → 𝑧𝑅𝑧)
9389, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9493adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑧𝑥) → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9585, 94syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥𝑧𝑥) → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96 eleq2 2687 . . . . . . . . . . . . . . . . . . . . 21 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
9796imbi1d 331 . . . . . . . . . . . . . . . . . . . 20 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ((𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9895, 97syl5ibcom 235 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9998imp 445 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧))
10079, 99syld 47 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
101100adantlll 753 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
10275, 101mtod 189 . . . . . . . . . . . . . . 15 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103102ex 450 . . . . . . . . . . . . . 14 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104103ralrimdva 2964 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∀𝑧𝑥 ¬ 𝑧𝑅𝑦))
105104reximdva 3012 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
106105adantll 749 . . . . . . . . . . 11 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
107106adantr 481 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
10869, 107mpd 15 . . . . . . . . 9 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
109108expl 647 . . . . . . . 8 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
110109alrimiv 1852 . . . . . . 7 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
111 df-fr 5038 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
112110, 111sylibr 224 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113 simpr 477 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114 df-we 5040 . . . . . 6 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
115112, 113, 114sylanbrc 697 . . . . 5 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 We 𝐴)
116 weinxp 5152 . . . . 5 (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117115, 116sylib 208 . . . 4 ((𝐴 ∈ FinII𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118 sqxpexg 6923 . . . . . 6 (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119 incom 3788 . . . . . . 7 (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120 inex1g 4766 . . . . . . 7 ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121119, 120syl5eqel 2702 . . . . . 6 ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122 weeq1 5067 . . . . . . 7 (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123122spcegv 3283 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124118, 121, 1233syl 18 . . . . 5 (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125124imp 445 . . . 4 ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126117, 125syldan 487 . . 3 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127 ween 8810 . . 3 (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128126, 127sylibr 224 . 2 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129 fin23 9163 . . . . 5 (𝐴 ∈ FinII𝐴 ∈ FinIII)
130 fin34 9164 . . . . 5 (𝐴 ∈ FinIII𝐴 ∈ FinIV)
131 fin45 9166 . . . . 5 (𝐴 ∈ FinIV𝐴 ∈ FinV)
132129, 130, 1313syl 18 . . . 4 (𝐴 ∈ FinII𝐴 ∈ FinV)
133 fin56 9167 . . . 4 (𝐴 ∈ FinV𝐴 ∈ FinVI)
134 fin67 9169 . . . 4 (𝐴 ∈ FinVI𝐴 ∈ FinVII)
135132, 133, 1343syl 18 . . 3 (𝐴 ∈ FinII𝐴 ∈ FinVII)
136 fin71num 9171 . . . 4 (𝐴 ∈ dom card → (𝐴 ∈ FinVII𝐴 ∈ Fin))
137136biimpac 503 . . 3 ((𝐴 ∈ FinVII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138135, 137sylan 488 . 2 ((𝐴 ∈ FinII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139128, 138syldan 487 1 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3o 1035  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135   cint 4445   class class class wbr 4618  cmpt 4678   Po wpo 4998   Or wor 4999   Fr wfr 5035   We wwe 5037   × cxp 5077  dom cdm 5079  ran crn 5080   [] crpss 6896  Fincfn 7907  cardccrd 8713  FinIIcfin2 9053  FinIVcfin4 9054  FinIIIcfin3 9055  FinVcfin5 9056  FinVIcfin6 9057  FinVIIcfin7 9058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-rpss 6897  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-seqom 7495  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-oi 8367  df-wdom 8416  df-card 8717  df-cda 8942  df-fin2 9060  df-fin4 9061  df-fin3 9062  df-fin5 9063  df-fin6 9064  df-fin7 9065
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator