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

Theorem fin2so 33526
 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 813 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2 ssrab2 3720 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥
3 sstr 3644 . . . . . . . . . . . . . . . . . . 19 (({𝑤𝑥𝑤𝑅𝑣} ⊆ 𝑥𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
42, 3mpan 706 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴)
5 elpw2g 4857 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ FinII → ({𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴))
65biimpar 501 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ FinII ∧ {𝑤𝑥𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
74, 6sylan2 490 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ FinII𝑥𝐴) → {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
87ralrimivw 2996 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
109rabex 4845 . . . . . . . . . . . . . . . . . 18 {𝑤𝑥𝑤𝑅𝑣} ∈ V
1110rgenw 2953 . . . . . . . . . . . . . . . . 17 𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V
12 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
13 eleq1 2718 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1412, 13ralrnmpt 6408 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴))
1511, 14ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ 𝒫 𝐴)
168, 15sylibr 224 . . . . . . . . . . . . . . 15 ((𝐴 ∈ FinII𝑥𝐴) → ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17 dfss3 3625 . . . . . . . . . . . . . . 15 (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
1816, 17sylibr 224 . . . . . . . . . . . . . 14 ((𝐴 ∈ FinII𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
1918adantlr 751 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2019adantr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
2110, 12dmmpti 6061 . . . . . . . . . . . . . . 15 dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = 𝑥
2221neeq1i 2887 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23 dm0rn0 5374 . . . . . . . . . . . . . . 15 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = ∅)
2423necon3bii 2875 . . . . . . . . . . . . . 14 (dom (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2522, 24sylbb1 227 . . . . . . . . . . . . 13 (𝑥 ≠ ∅ → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
2625adantl 481 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅)
27 soss 5082 . . . . . . . . . . . . . . . 16 (𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝑥))
2827impcom 445 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝑥𝐴) → 𝑅 Or 𝑥)
29 porpss 6983 . . . . . . . . . . . . . . . . 17 [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})
3029a1i 11 . . . . . . . . . . . . . . . 16 (𝑅 Or 𝑥 → [] Po ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
31 solin 5087 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣))
32 fin2solem 33525 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣𝑅𝑦 → {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
33 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑦 → (𝑤𝑅𝑣𝑤𝑅𝑦))
3433rabbidv 3220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦})
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑣 = 𝑦 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
36 fin2solem 33525 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Or 𝑥 ∧ (𝑦𝑥𝑣𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3736ancom2s 861 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → (𝑦𝑅𝑣 → {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
3832, 35, 373orim123d 1447 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ((𝑣𝑅𝑦𝑣 = 𝑦𝑦𝑅𝑣) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
3931, 38mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Or 𝑥 ∧ (𝑣𝑥𝑦𝑥)) → ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4039ralrimivva 3000 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 Or 𝑥 → ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
41 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦}))
42 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (𝑢 = {𝑤𝑥𝑤𝑅𝑦} ↔ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦}))
43 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ({𝑤𝑥𝑤𝑅𝑦} [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4441, 42, 433orbi123d 1438 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → ((𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4544ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = {𝑤𝑥𝑤𝑅𝑣} → (∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4612, 45ralrnmpt 6408 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣})))
4711, 46ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢) ↔ ∀𝑣𝑥𝑦𝑥 ({𝑤𝑥𝑤𝑅𝑣} [] {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] {𝑤𝑥𝑤𝑅𝑣}))
4840, 47sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
4948r19.21bi 2961 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
509rabex 4845 . . . . . . . . . . . . . . . . . . . . 21 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5150rgenw 2953 . . . . . . . . . . . . . . . . . . . 20 𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V
5234cbvmptv 4783 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = (𝑦𝑥 ↦ {𝑤𝑥𝑤𝑅𝑦})
53 breq2 4689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 [] 𝑧𝑢 [] {𝑤𝑥𝑤𝑅𝑦}))
54 eqeq2 2662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑢 = 𝑧𝑢 = {𝑤𝑥𝑤𝑅𝑦}))
55 breq1 4688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 [] 𝑢 ↔ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5653, 54, 553orbi123d 1438 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = {𝑤𝑥𝑤𝑅𝑦} → ((𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5752, 56ralrnmpt 6408 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦𝑥 {𝑤𝑥𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢)))
5851, 57ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢) ↔ ∀𝑦𝑥 (𝑢 [] {𝑤𝑥𝑤𝑅𝑦} ∨ 𝑢 = {𝑤𝑥𝑤𝑅𝑦} ∨ {𝑤𝑥𝑤𝑅𝑦} [] 𝑢))
5949, 58sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})(𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6059r19.21bi 2961 . . . . . . . . . . . . . . . . 17 (((𝑅 Or 𝑥𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6160anasss 680 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → (𝑢 [] 𝑧𝑢 = 𝑧𝑧 [] 𝑢))
6230, 61issod 5094 . . . . . . . . . . . . . . 15 (𝑅 Or 𝑥 → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6328, 62syl 17 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6463adantll 750 . . . . . . . . . . . . 13 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6564adantr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
66 fin2i2 9178 . . . . . . . . . . . 12 (((𝐴 ∈ FinII ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ≠ ∅ ∧ [] Or ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
671, 20, 26, 65, 66syl22anc 1367 . . . . . . . . . . 11 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}))
6852, 50elrnmpti 5408 . . . . . . . . . . 11 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
6967, 68sylib 208 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦})
70 ssel2 3631 . . . . . . . . . . . . . . . . . . . 20 ((𝑥𝐴𝑧𝑥) → 𝑧𝐴)
71 sonr 5085 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Or 𝐴𝑧𝐴) → ¬ 𝑧𝑅𝑧)
7270, 71sylan2 490 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑧𝑥)) → ¬ 𝑧𝑅𝑧)
7372anassrs 681 . . . . . . . . . . . . . . . . . 18 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7473adantlr 751 . . . . . . . . . . . . . . . . 17 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ¬ 𝑧𝑅𝑧)
7574adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76 breq1 4688 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (𝑤𝑅𝑦𝑧𝑅𝑦))
7776elrab 3396 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} ↔ (𝑧𝑥𝑧𝑅𝑦))
7877simplbi2 654 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
7978ad2antlr 763 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
80 vex 3234 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
8180elint2 4514 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦)
82 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = {𝑤𝑥𝑤𝑅𝑣} → (𝑧𝑦𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8312, 82ralrnmpt 6408 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑣𝑥 {𝑤𝑥𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣}))
8411, 83ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦 ∈ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣})𝑧𝑦 ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
8581, 84bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ ∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣})
86 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = 𝑧 → (𝑤𝑅𝑣𝑤𝑅𝑧))
8786rabbidv 3220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → {𝑤𝑥𝑤𝑅𝑣} = {𝑤𝑥𝑤𝑅𝑧})
8887eleq2d 2716 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
8988rspcv 3336 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧}))
90 breq1 4688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → (𝑤𝑅𝑧𝑧𝑅𝑧))
9190elrab 3396 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} ↔ (𝑧𝑥𝑧𝑅𝑧))
9291simprbi 479 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑧} → 𝑧𝑅𝑧)
9389, 92syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑥 → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9493adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑥𝑧𝑥) → (∀𝑣𝑥 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑣} → 𝑧𝑅𝑧))
9585, 94syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑥𝑧𝑥) → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96 eleq2 2719 . . . . . . . . . . . . . . . . . . . . 21 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦}))
9796imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ((𝑧 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9895, 97syl5ibcom 235 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑥𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
9998imp 444 . . . . . . . . . . . . . . . . . 18 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤𝑥𝑤𝑅𝑦} → 𝑧𝑅𝑧))
10079, 99syld 47 . . . . . . . . . . . . . . . . 17 (((𝑦𝑥𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
101100adantlll 754 . . . . . . . . . . . . . . . 16 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → (𝑧𝑅𝑦𝑧𝑅𝑧))
10275, 101mtod 189 . . . . . . . . . . . . . . 15 (((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) ∧ ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103102ex 449 . . . . . . . . . . . . . 14 ((((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) ∧ 𝑧𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104103ralrimdva 2998 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝑥) → ( ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∀𝑧𝑥 ¬ 𝑧𝑅𝑦))
105104reximdva 3046 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
106105adantll 750 . . . . . . . . . . 11 (((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
107106adantr 480 . . . . . . . . . 10 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦𝑥 ran (𝑣𝑥 ↦ {𝑤𝑥𝑤𝑅𝑣}) = {𝑤𝑥𝑤𝑅𝑦} → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
10869, 107mpd 15 . . . . . . . . 9 ((((𝐴 ∈ FinII𝑅 Or 𝐴) ∧ 𝑥𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
109108expl 647 . . . . . . . 8 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
110109alrimiv 1895 . . . . . . 7 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
111 df-fr 5102 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
112110, 111sylibr 224 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113 simpr 476 . . . . . 6 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114 df-we 5104 . . . . . 6 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
115112, 113, 114sylanbrc 699 . . . . 5 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝑅 We 𝐴)
116 weinxp 5220 . . . . 5 (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117115, 116sylib 208 . . . 4 ((𝐴 ∈ FinII𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118 sqxpexg 7005 . . . . . 6 (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119 incom 3838 . . . . . . 7 (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120 inex1g 4834 . . . . . . 7 ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121119, 120syl5eqel 2734 . . . . . 6 ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122 weeq1 5131 . . . . . . 7 (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123122spcegv 3325 . . . . . 6 ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124118, 121, 1233syl 18 . . . . 5 (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125124imp 444 . . . 4 ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126117, 125syldan 486 . . 3 ((𝐴 ∈ FinII𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127 ween 8896 . . 3 (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128126, 127sylibr 224 . 2 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129 fin23 9249 . . . . 5 (𝐴 ∈ FinII𝐴 ∈ FinIII)
130 fin34 9250 . . . . 5 (𝐴 ∈ FinIII𝐴 ∈ FinIV)
131 fin45 9252 . . . . 5 (𝐴 ∈ FinIV𝐴 ∈ FinV)
132129, 130, 1313syl 18 . . . 4 (𝐴 ∈ FinII𝐴 ∈ FinV)
133 fin56 9253 . . . 4 (𝐴 ∈ FinV𝐴 ∈ FinVI)
134 fin67 9255 . . . 4 (𝐴 ∈ FinVI𝐴 ∈ FinVII)
135132, 133, 1343syl 18 . . 3 (𝐴 ∈ FinII𝐴 ∈ FinVII)
136 fin71num 9257 . . . 4 (𝐴 ∈ dom card → (𝐴 ∈ FinVII𝐴 ∈ Fin))
137136biimpac 502 . . 3 ((𝐴 ∈ FinVII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138135, 137sylan 487 . 2 ((𝐴 ∈ FinII𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139128, 138syldan 486 1 ((𝐴 ∈ FinII𝑅 Or 𝐴) → 𝐴 ∈ Fin)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∨ w3o 1053  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  ∩ cint 4507   class class class wbr 4685   ↦ cmpt 4762   Po wpo 5062   Or wor 5063   Fr wfr 5099   We wwe 5101   × cxp 5141  dom cdm 5143  ran crn 5144   [⊊] crpss 6978  Fincfn 7997  cardccrd 8799  FinIIcfin2 9139  FinIVcfin4 9140  FinIIIcfin3 9141  FinVcfin5 9142  FinVIcfin6 9143  FinVIIcfin7 9144 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-rpss 6979  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-seqom 7588  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-wdom 8505  df-card 8803  df-cda 9028  df-fin2 9146  df-fin4 9147  df-fin3 9148  df-fin5 9149  df-fin6 9150  df-fin7 9151 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator