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 33729
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 750 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2 ssrab2 3836 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥
3 sstr 3760 . . . . . . . . . . . . . . . . . . 19 (({𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
42, 3mpan 662 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
5 elpw2g 4958 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ FinII → ({𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴))
65biimpar 463 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ FinII ∧ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
74, 6sylan2 572 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ FinII𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
87ralrimivw 3116 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
109rabex 4946 . . . . . . . . . . . . . . . . . 18 {𝑤𝑥𝑤𝑅𝑣} ∈ V
1110rgenw 3073 . . . . . . . . . . . . . . . . 17 𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V
12 eqid 2771 . . . . . . . . . . . . . . . . . 18 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
13 eleq1 2838 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1412, 13ralrnmpt 6511 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1511, 14ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
168, 15sylibr 224 . . . . . . . . . . . . . . 15 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17 dfss3 3741 . . . . . . . . . . . . . . 15 (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
1816, 17sylibr 224 . . . . . . . . . . . . . 14 ((𝐴 ∈ FinII𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
1918adantlr 686 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2019adantr 466 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2110, 12dmmpti 6163 . . . . . . . . . . . . . . 15 dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = 𝑥
2221neeq1i 3007 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23 dm0rn0 5480 . . . . . . . . . . . . . . 15 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅)
2423necon3bii 2995 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2522, 24sylbb1 227 . . . . . . . . . . . . 13 (𝑥 ≠ ∅ → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2625adantl 467 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
27 soss 5188 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝑥))
2827impcom 394 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝑥𝐴) → 𝑅 Or 𝑥)
29 porpss 7088 . . . . . . . . . . . . . . . . 17 [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
3029a1i 11 . . . . . . . . . . . . . . . 16 (𝑅 Or 𝑥 → [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
31 solin 5193 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣))
32 fin2solem 33728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦 → {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
33 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑦 → (𝑤𝑅𝑣𝑤𝑅𝑦))
3433rabbidv 3339 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦})
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
36 fin2solem 33728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑣𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3736ancom2s 621 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3832, 35, 373orim123d 1555 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ((𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
3931, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4039ralrimivva 3120 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Or 𝑥 → ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
41 breq1 4789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
42 eqeq1 2775 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 = {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
43 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ({𝑤𝑥𝑤𝑅𝑦} [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4441, 42, 433orbi123d 1546 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ((𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4544ralbidv 3135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4612, 45ralrnmpt 6511 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4711, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4840, 47sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
4948r19.21bi 3081 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
509rabex 4946 . . . . . . . . . . . . . . . . . . . . 21 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5150rgenw 3073 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5234cbvmptv 4884 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑦𝑥 ↦ {𝑤𝑥𝑤𝑅𝑦})
53 breq2 4790 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 [] 𝑧𝑢 [] {𝑤𝑥𝑤𝑅𝑦}))
54 eqeq2 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 = 𝑧𝑢 = {𝑤𝑥𝑤𝑅𝑦}))
55 breq1 4789 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5653, 54, 553orbi123d 1546 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → ((𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5752, 56ralrnmpt 6511 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5851, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5949, 58sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6059r19.21bi 3081 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6160anasss 457 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6230, 61issod 5200 . . . . . . . . . . . . . . 15 (𝑅 Or 𝑥 → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6328, 62syl 17 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6463adantll 685 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6564adantr 466 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
66 fin2i2 9342 . . . . . . . . . . . 12 (((𝐴 ∈ FinII ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ∧ [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
671, 20, 26, 65, 66syl22anc 1477 . . . . . . . . . . 11 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6852, 50elrnmpti 5514 . . . . . . . . . . 11 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
6967, 68sylib 208 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
70 ssel2 3747 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧𝑥) → 𝑧𝐴)
71 sonr 5191 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴𝑧𝐴) → ¬ 𝑧𝑅𝑧)
7270, 71sylan2 572 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑧𝑥)) → ¬ 𝑧𝑅𝑧)
7372anassrs 458 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7473adantlr 686 . . . . . . . . . . . . . . . . 17 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7574adantr 466 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76 breq1 4789 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑤𝑅𝑦𝑧𝑅𝑦))
7776elrab 3515 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} ↔ (𝑧𝑥𝑧𝑅𝑦))
7877simplbi2 482 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
7978ad2antlr 698 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
80 vex 3354 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
8180elint2 4618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦)
82 eleq2 2839 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑧𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8312, 82ralrnmpt 6511 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8411, 83ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
8581, 84bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
86 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑧 → (𝑤𝑅𝑣𝑤𝑅𝑧))
8786rabbidv 3339 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑧})
8887eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
8988rspcv 3456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
90 breq1 4789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑅𝑧𝑧𝑅𝑧))
9190elrab 3515 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} ↔ (𝑧𝑥𝑧𝑅𝑧))
9291simprbi 478 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} → 𝑧𝑅𝑧)
9389, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9493adantl 467 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑧𝑥) → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9585, 94syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥𝑧𝑥) → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96 eleq2 2839 . . . . . . . . . . . . . . . . . . . . 21 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
9796imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ((𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9895, 97syl5ibcom 235 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9998imp 393 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧))
10079, 99syld 47 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
101100adantlll 689 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
10275, 101mtod 189 . . . . . . . . . . . . . . 15 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103102ex 397 . . . . . . . . . . . . . 14 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104103ralrimdva 3118 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∀𝑧𝑥 ¬ 𝑧𝑅𝑦))
105104reximdva 3165 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
106105adantll 685 . . . . . . . . . . 11 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
107106adantr 466 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
10869, 107mpd 15 . . . . . . . . 9 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
109108expl 445 . . . . . . . 8 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
110109alrimiv 2007 . . . . . . 7 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
111 df-fr 5208 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
112110, 111sylibr 224 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113 simpr 471 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114 df-we 5210 . . . . . 6 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
115112, 113, 114sylanbrc 564 . . . . 5 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 We 𝐴)
116 weinxp 5326 . . . . 5 (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117115, 116sylib 208 . . . 4 ((𝐴 ∈ FinII𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118 sqxpexg 7110 . . . . . 6 (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119 incom 3956 . . . . . . 7 (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120 inex1g 4935 . . . . . . 7 ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121119, 120syl5eqel 2854 . . . . . 6 ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122 weeq1 5237 . . . . . . 7 (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123122spcegv 3445 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124118, 121, 1233syl 18 . . . . 5 (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125124imp 393 . . . 4 ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126117, 125syldan 571 . . 3 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127 ween 9058 . . 3 (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128126, 127sylibr 224 . 2 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129 fin23 9413 . . . . 5 (𝐴 ∈ FinII𝐴 ∈ FinIII)
130 fin34 9414 . . . . 5 (𝐴 ∈ FinIII𝐴 ∈ FinIV)
131 fin45 9416 . . . . 5 (𝐴 ∈ FinIV𝐴 ∈ FinV)
132129, 130, 1313syl 18 . . . 4 (𝐴 ∈ FinII𝐴 ∈ FinV)
133 fin56 9417 . . . 4 (𝐴 ∈ FinV𝐴 ∈ FinVI)
134 fin67 9419 . . . 4 (𝐴 ∈ FinVI𝐴 ∈ FinVII)
135132, 133, 1343syl 18 . . 3 (𝐴 ∈ FinII𝐴 ∈ FinVII)
136 fin71num 9421 . . . 4 (𝐴 ∈ dom card → (𝐴 ∈ FinVII𝐴 ∈ Fin))
137136biimpac 464 . . 3 ((𝐴 ∈ FinVII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138135, 137sylan 561 . 2 ((𝐴 ∈ FinII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139128, 138syldan 571 1 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3o 1070  wal 1629   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297   cint 4611   class class class wbr 4786  cmpt 4863   Po wpo 5168   Or wor 5169   Fr wfr 5205   We wwe 5207   × cxp 5247  dom cdm 5249  ran crn 5250   [] crpss 7083  Fincfn 8109  cardccrd 8961  FinIIcfin2 9303  FinIVcfin4 9304  FinIIIcfin3 9305  FinVcfin5 9306  FinVIcfin6 9307  FinVIIcfin7 9308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-rpss 7084  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-seqom 7696  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-oi 8571  df-wdom 8620  df-card 8965  df-cda 9192  df-fin2 9310  df-fin4 9311  df-fin3 9312  df-fin5 9313  df-fin6 9314  df-fin7 9315
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator