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 37593
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 775 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2 ssrab2 4089 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥
3 sstr 4003 . . . . . . . . . . . . . . . . . . 19 (({𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
42, 3mpan 690 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
5 elpw2g 5338 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ FinII → ({𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴))
65biimpar 477 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ FinII ∧ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
74, 6sylan2 593 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ FinII𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
87ralrimivw 3147 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9 vex 3481 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
109rabex 5344 . . . . . . . . . . . . . . . . . 18 {𝑤𝑥𝑤𝑅𝑣} ∈ V
1110rgenw 3062 . . . . . . . . . . . . . . . . 17 𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V
12 eqid 2734 . . . . . . . . . . . . . . . . . 18 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
13 eleq1 2826 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1412, 13ralrnmptw 7113 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1511, 14ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
168, 15sylibr 234 . . . . . . . . . . . . . . 15 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17 dfss3 3983 . . . . . . . . . . . . . . 15 (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
1816, 17sylibr 234 . . . . . . . . . . . . . 14 ((𝐴 ∈ FinII𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
1918adantlr 715 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2019adantr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2110, 12dmmpti 6712 . . . . . . . . . . . . . . 15 dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = 𝑥
2221neeq1i 3002 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23 dm0rn0 5937 . . . . . . . . . . . . . . 15 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅)
2423necon3bii 2990 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2522, 24sylbb1 237 . . . . . . . . . . . . 13 (𝑥 ≠ ∅ → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2625adantl 481 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
27 soss 5616 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝑥))
2827impcom 407 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝑥𝐴) → 𝑅 Or 𝑥)
29 porpss 7745 . . . . . . . . . . . . . . . . 17 [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
3029a1i 11 . . . . . . . . . . . . . . . 16 (𝑅 Or 𝑥 → [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
31 solin 5622 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣))
32 fin2solem 37592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦 → {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
33 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑦 → (𝑤𝑅𝑣𝑤𝑅𝑦))
3433rabbidv 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦})
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
36 fin2solem 37592 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑣𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3736ancom2s 650 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3832, 35, 373orim123d 1443 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ((𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
3931, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4039ralrimivva 3199 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Or 𝑥 → ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
41 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
42 eqeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 = {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
43 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ({𝑤𝑥𝑤𝑅𝑦} [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4441, 42, 433orbi123d 1434 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ((𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4544ralbidv 3175 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4612, 45ralrnmptw 7113 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4711, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4840, 47sylibr 234 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
4948r19.21bi 3248 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
509rabex 5344 . . . . . . . . . . . . . . . . . . . . 21 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5150rgenw 3062 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5234cbvmptv 5260 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑦𝑥 ↦ {𝑤𝑥𝑤𝑅𝑦})
53 breq2 5151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 [] 𝑧𝑢 [] {𝑤𝑥𝑤𝑅𝑦}))
54 eqeq2 2746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 = 𝑧𝑢 = {𝑤𝑥𝑤𝑅𝑦}))
55 breq1 5150 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5653, 54, 553orbi123d 1434 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → ((𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5752, 56ralrnmptw 7113 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5851, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5949, 58sylibr 234 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6059r19.21bi 3248 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6160anasss 466 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6230, 61issod 5630 . . . . . . . . . . . . . . 15 (𝑅 Or 𝑥 → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6328, 62syl 17 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6463adantll 714 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6564adantr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
66 fin2i2 10355 . . . . . . . . . . . 12 (((𝐴 ∈ FinII ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ∧ [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
671, 20, 26, 65, 66syl22anc 839 . . . . . . . . . . 11 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6852, 50elrnmpti 5975 . . . . . . . . . . 11 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
6967, 68sylib 218 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
70 ssel2 3989 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧𝑥) → 𝑧𝐴)
71 sonr 5620 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴𝑧𝐴) → ¬ 𝑧𝑅𝑧)
7270, 71sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑧𝑥)) → ¬ 𝑧𝑅𝑧)
7372anassrs 467 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7473adantlr 715 . . . . . . . . . . . . . . . . 17 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7574adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76 breq1 5150 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑤𝑅𝑦𝑧𝑅𝑦))
7776elrab 3694 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} ↔ (𝑧𝑥𝑧𝑅𝑦))
7877simplbi2 500 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
7978ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
80 vex 3481 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
8180elint2 4957 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦)
82 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑧𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8312, 82ralrnmptw 7113 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8411, 83ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
8581, 84bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
86 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑧 → (𝑤𝑅𝑣𝑤𝑅𝑧))
8786rabbidv 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑧})
8887eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
8988rspcv 3617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
90 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑅𝑧𝑧𝑅𝑧))
9190elrab 3694 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} ↔ (𝑧𝑥𝑧𝑅𝑧))
9291simprbi 496 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} → 𝑧𝑅𝑧)
9389, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9493adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑧𝑥) → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9585, 94biimtrid 242 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥𝑧𝑥) → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96 eleq2 2827 . . . . . . . . . . . . . . . . . . . . 21 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
9796imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ((𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9895, 97syl5ibcom 245 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9998imp 406 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧))
10079, 99syld 47 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
101100adantlll 718 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
10275, 101mtod 198 . . . . . . . . . . . . . . 15 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103102ex 412 . . . . . . . . . . . . . 14 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104103ralrimdva 3151 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∀𝑧𝑥 ¬ 𝑧𝑅𝑦))
105104reximdva 3165 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
106105adantll 714 . . . . . . . . . . 11 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
107106adantr 480 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
10869, 107mpd 15 . . . . . . . . 9 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
109108expl 457 . . . . . . . 8 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
110109alrimiv 1924 . . . . . . 7 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
111 df-fr 5640 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
112110, 111sylibr 234 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113 simpr 484 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114 df-we 5642 . . . . . 6 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
115112, 113, 114sylanbrc 583 . . . . 5 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 We 𝐴)
116 weinxp 5772 . . . . 5 (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117115, 116sylib 218 . . . 4 ((𝐴 ∈ FinII𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118 sqxpexg 7773 . . . . . 6 (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119 incom 4216 . . . . . . 7 (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120 inex1g 5324 . . . . . . 7 ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121119, 120eqeltrid 2842 . . . . . 6 ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122 weeq1 5675 . . . . . . 7 (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123122spcegv 3596 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124118, 121, 1233syl 18 . . . . 5 (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125124imp 406 . . . 4 ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126117, 125syldan 591 . . 3 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127 ween 10072 . . 3 (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128126, 127sylibr 234 . 2 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129 fin23 10426 . . . . 5 (𝐴 ∈ FinII𝐴 ∈ FinIII)
130 fin34 10427 . . . . 5 (𝐴 ∈ FinIII𝐴 ∈ FinIV)
131 fin45 10429 . . . . 5 (𝐴 ∈ FinIV𝐴 ∈ FinV)
132129, 130, 1313syl 18 . . . 4 (𝐴 ∈ FinII𝐴 ∈ FinV)
133 fin56 10430 . . . 4 (𝐴 ∈ FinV𝐴 ∈ FinVI)
134 fin67 10432 . . . 4 (𝐴 ∈ FinVI𝐴 ∈ FinVII)
135132, 133, 1343syl 18 . . 3 (𝐴 ∈ FinII𝐴 ∈ FinVII)
136 fin71num 10434 . . . 4 (𝐴 ∈ dom card → (𝐴 ∈ FinVII𝐴 ∈ Fin))
137136biimpac 478 . . 3 ((𝐴 ∈ FinVII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138135, 137sylan 580 . 2 ((𝐴 ∈ FinII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139128, 138syldan 591 1 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3o 1085  wal 1534   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604   cint 4950   class class class wbr 5147  cmpt 5230   Po wpo 5594   Or wor 5595   Fr wfr 5637   We wwe 5639   × cxp 5686  dom cdm 5688  ran crn 5689   [] crpss 7740  Fincfn 8983  cardccrd 9972  FinIIcfin2 10316  FinIVcfin4 10317  FinIIIcfin3 10318  FinVcfin5 10319  FinVIcfin6 10320  FinVIIcfin7 10321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-rpss 7741  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-seqom 8486  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-oi 9547  df-wdom 9602  df-dju 9938  df-card 9976  df-fin2 10323  df-fin4 10324  df-fin3 10325  df-fin5 10326  df-fin6 10327  df-fin7 10328
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator