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 33820
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 791 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2 ssrab2 3847 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥
3 sstr 3769 . . . . . . . . . . . . . . . . . . 19 (({𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
42, 3mpan 681 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
5 elpw2g 4985 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ FinII → ({𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴))
65biimpar 469 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ FinII ∧ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
74, 6sylan2 586 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ FinII𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
87ralrimivw 3114 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
109rabex 4973 . . . . . . . . . . . . . . . . . 18 {𝑤𝑥𝑤𝑅𝑣} ∈ V
1110rgenw 3071 . . . . . . . . . . . . . . . . 17 𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V
12 eqid 2765 . . . . . . . . . . . . . . . . . 18 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
13 eleq1 2832 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1412, 13ralrnmpt 6558 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1511, 14ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
168, 15sylibr 225 . . . . . . . . . . . . . . 15 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17 dfss3 3750 . . . . . . . . . . . . . . 15 (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
1816, 17sylibr 225 . . . . . . . . . . . . . 14 ((𝐴 ∈ FinII𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
1918adantlr 706 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2019adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2110, 12dmmpti 6201 . . . . . . . . . . . . . . 15 dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = 𝑥
2221neeq1i 3001 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23 dm0rn0 5510 . . . . . . . . . . . . . . 15 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅)
2423necon3bii 2989 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2522, 24sylbb1 228 . . . . . . . . . . . . 13 (𝑥 ≠ ∅ → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2625adantl 473 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
27 soss 5216 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝑥))
2827impcom 396 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝑥𝐴) → 𝑅 Or 𝑥)
29 porpss 7139 . . . . . . . . . . . . . . . . 17 [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
3029a1i 11 . . . . . . . . . . . . . . . 16 (𝑅 Or 𝑥 → [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
31 solin 5221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣))
32 fin2solem 33819 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦 → {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
33 breq2 4813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑦 → (𝑤𝑅𝑣𝑤𝑅𝑦))
3433rabbidv 3338 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦})
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
36 fin2solem 33819 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑣𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3736ancom2s 640 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3832, 35, 373orim123d 1568 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ((𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
3931, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4039ralrimivva 3118 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Or 𝑥 → ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
41 breq1 4812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
42 eqeq1 2769 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 = {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
43 breq2 4813 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ({𝑤𝑥𝑤𝑅𝑦} [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4441, 42, 433orbi123d 1559 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ((𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4544ralbidv 3133 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4612, 45ralrnmpt 6558 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4711, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4840, 47sylibr 225 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
4948r19.21bi 3079 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
509rabex 4973 . . . . . . . . . . . . . . . . . . . . 21 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5150rgenw 3071 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5234cbvmptv 4909 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑦𝑥 ↦ {𝑤𝑥𝑤𝑅𝑦})
53 breq2 4813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 [] 𝑧𝑢 [] {𝑤𝑥𝑤𝑅𝑦}))
54 eqeq2 2776 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 = 𝑧𝑢 = {𝑤𝑥𝑤𝑅𝑦}))
55 breq1 4812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5653, 54, 553orbi123d 1559 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → ((𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5752, 56ralrnmpt 6558 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5851, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5949, 58sylibr 225 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6059r19.21bi 3079 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6160anasss 458 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6230, 61issod 5228 . . . . . . . . . . . . . . 15 (𝑅 Or 𝑥 → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6328, 62syl 17 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6463adantll 705 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6564adantr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
66 fin2i2 9393 . . . . . . . . . . . 12 (((𝐴 ∈ FinII ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ∧ [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
671, 20, 26, 65, 66syl22anc 867 . . . . . . . . . . 11 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6852, 50elrnmpti 5545 . . . . . . . . . . 11 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
6967, 68sylib 209 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
70 ssel2 3756 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧𝑥) → 𝑧𝐴)
71 sonr 5219 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴𝑧𝐴) → ¬ 𝑧𝑅𝑧)
7270, 71sylan2 586 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑧𝑥)) → ¬ 𝑧𝑅𝑧)
7372anassrs 459 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7473adantlr 706 . . . . . . . . . . . . . . . . 17 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7574adantr 472 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76 breq1 4812 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑤𝑅𝑦𝑧𝑅𝑦))
7776elrab 3519 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} ↔ (𝑧𝑥𝑧𝑅𝑦))
7877simplbi2 494 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
7978ad2antlr 718 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
80 vex 3353 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
8180elint2 4640 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦)
82 eleq2 2833 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑧𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8312, 82ralrnmpt 6558 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8411, 83ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
8581, 84bitri 266 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
86 breq2 4813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑧 → (𝑤𝑅𝑣𝑤𝑅𝑧))
8786rabbidv 3338 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑧})
8887eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
8988rspcv 3457 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
90 breq1 4812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑅𝑧𝑧𝑅𝑧))
9190elrab 3519 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} ↔ (𝑧𝑥𝑧𝑅𝑧))
9291simprbi 490 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} → 𝑧𝑅𝑧)
9389, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9493adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑧𝑥) → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9585, 94syl5bi 233 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥𝑧𝑥) → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96 eleq2 2833 . . . . . . . . . . . . . . . . . . . . 21 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
9796imbi1d 332 . . . . . . . . . . . . . . . . . . . 20 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ((𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9895, 97syl5ibcom 236 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9998imp 395 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧))
10079, 99syld 47 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
101100adantlll 709 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
10275, 101mtod 189 . . . . . . . . . . . . . . 15 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103102ex 401 . . . . . . . . . . . . . 14 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104103ralrimdva 3116 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∀𝑧𝑥 ¬ 𝑧𝑅𝑦))
105104reximdva 3163 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
106105adantll 705 . . . . . . . . . . 11 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
107106adantr 472 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
10869, 107mpd 15 . . . . . . . . 9 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
109108expl 449 . . . . . . . 8 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
110109alrimiv 2022 . . . . . . 7 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
111 df-fr 5236 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
112110, 111sylibr 225 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113 simpr 477 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114 df-we 5238 . . . . . 6 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
115112, 113, 114sylanbrc 578 . . . . 5 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 We 𝐴)
116 weinxp 5356 . . . . 5 (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117115, 116sylib 209 . . . 4 ((𝐴 ∈ FinII𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118 sqxpexg 7161 . . . . . 6 (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119 incom 3967 . . . . . . 7 (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120 inex1g 4962 . . . . . . 7 ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121119, 120syl5eqel 2848 . . . . . 6 ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122 weeq1 5265 . . . . . . 7 (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123122spcegv 3446 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124118, 121, 1233syl 18 . . . . 5 (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125124imp 395 . . . 4 ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126117, 125syldan 585 . . 3 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127 ween 9109 . . 3 (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128126, 127sylibr 225 . 2 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129 fin23 9464 . . . . 5 (𝐴 ∈ FinII𝐴 ∈ FinIII)
130 fin34 9465 . . . . 5 (𝐴 ∈ FinIII𝐴 ∈ FinIV)
131 fin45 9467 . . . . 5 (𝐴 ∈ FinIV𝐴 ∈ FinV)
132129, 130, 1313syl 18 . . . 4 (𝐴 ∈ FinII𝐴 ∈ FinV)
133 fin56 9468 . . . 4 (𝐴 ∈ FinV𝐴 ∈ FinVI)
134 fin67 9470 . . . 4 (𝐴 ∈ FinVI𝐴 ∈ FinVII)
135132, 133, 1343syl 18 . . 3 (𝐴 ∈ FinII𝐴 ∈ FinVII)
136 fin71num 9472 . . . 4 (𝐴 ∈ dom card → (𝐴 ∈ FinVII𝐴 ∈ Fin))
137136biimpac 470 . . 3 ((𝐴 ∈ FinVII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138135, 137sylan 575 . 2 ((𝐴 ∈ FinII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139128, 138syldan 585 1 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3o 1106  wal 1650   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   cint 4633   class class class wbr 4809  cmpt 4888   Po wpo 5196   Or wor 5197   Fr wfr 5233   We wwe 5235   × cxp 5275  dom cdm 5277  ran crn 5278   [] crpss 7134  Fincfn 8160  cardccrd 9012  FinIIcfin2 9354  FinIVcfin4 9355  FinIIIcfin3 9356  FinVcfin5 9357  FinVIcfin6 9358  FinVIIcfin7 9359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-rpss 7135  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-seqom 7747  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-oi 8622  df-wdom 8671  df-card 9016  df-cda 9243  df-fin2 9361  df-fin4 9362  df-fin3 9363  df-fin5 9364  df-fin6 9365  df-fin7 9366
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator