MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin1a2lem7 Structured version   Visualization version   GIF version

Theorem fin1a2lem7 9440
Description: Lemma for fin1a2 9449. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
Hypotheses
Ref Expression
fin1a2lem.b 𝐸 = (𝑥 ∈ ω ↦ (2𝑜 ·𝑜 𝑥))
fin1a2lem.aa 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
Assertion
Ref Expression
fin1a2lem7 ((𝐴𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII)) → 𝐴 ∈ FinIII)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐸
Allowed substitution hints:   𝐴(𝑥)   𝑆(𝑥,𝑦)   𝐸(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem fin1a2lem7
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 peano1 7251 . . . . . 6 ∅ ∈ ω
2 ne0i 4064 . . . . . 6 (∅ ∈ ω → ω ≠ ∅)
3 brwdomn0 8641 . . . . . 6 (ω ≠ ∅ → (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴onto→ω))
41, 2, 3mp2b 10 . . . . 5 (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴onto→ω)
5 vex 3343 . . . . . . . . . 10 𝑓 ∈ V
6 fof 6277 . . . . . . . . . 10 (𝑓:𝐴onto→ω → 𝑓:𝐴⟶ω)
7 dmfex 7290 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V)
85, 6, 7sylancr 698 . . . . . . . . 9 (𝑓:𝐴onto→ω → 𝐴 ∈ V)
9 cnvimass 5643 . . . . . . . . . 10 (𝑓 “ ran 𝐸) ⊆ dom 𝑓
10 fdm 6212 . . . . . . . . . . 11 (𝑓:𝐴⟶ω → dom 𝑓 = 𝐴)
116, 10syl 17 . . . . . . . . . 10 (𝑓:𝐴onto→ω → dom 𝑓 = 𝐴)
129, 11syl5sseq 3794 . . . . . . . . 9 (𝑓:𝐴onto→ω → (𝑓 “ ran 𝐸) ⊆ 𝐴)
138, 12sselpwd 4959 . . . . . . . 8 (𝑓:𝐴onto→ω → (𝑓 “ ran 𝐸) ∈ 𝒫 𝐴)
14 fin1a2lem.b . . . . . . . . . . . . . 14 𝐸 = (𝑥 ∈ ω ↦ (2𝑜 ·𝑜 𝑥))
1514fin1a2lem4 9437 . . . . . . . . . . . . 13 𝐸:ω–1-1→ω
16 f1cnv 6322 . . . . . . . . . . . . 13 (𝐸:ω–1-1→ω → 𝐸:ran 𝐸1-1-onto→ω)
17 f1ofo 6306 . . . . . . . . . . . . 13 (𝐸:ran 𝐸1-1-onto→ω → 𝐸:ran 𝐸onto→ω)
1815, 16, 17mp2b 10 . . . . . . . . . . . 12 𝐸:ran 𝐸onto→ω
19 fofun 6278 . . . . . . . . . . . 12 (𝐸:ran 𝐸onto→ω → Fun 𝐸)
2018, 19ax-mp 5 . . . . . . . . . . 11 Fun 𝐸
215resex 5601 . . . . . . . . . . 11 (𝑓 ↾ (𝑓 “ ran 𝐸)) ∈ V
22 cofunexg 7296 . . . . . . . . . . 11 ((Fun 𝐸 ∧ (𝑓 ↾ (𝑓 “ ran 𝐸)) ∈ V) → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V)
2320, 21, 22mp2an 710 . . . . . . . . . 10 (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V
24 fofun 6278 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → Fun 𝑓)
25 fores 6286 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)))
2624, 9, 25sylancl 697 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)))
27 f1f 6262 . . . . . . . . . . . . . . 15 (𝐸:ω–1-1→ω → 𝐸:ω⟶ω)
28 frn 6214 . . . . . . . . . . . . . . 15 (𝐸:ω⟶ω → ran 𝐸 ⊆ ω)
2915, 27, 28mp2b 10 . . . . . . . . . . . . . 14 ran 𝐸 ⊆ ω
30 foimacnv 6316 . . . . . . . . . . . . . 14 ((𝑓:𝐴onto→ω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸)
3129, 30mpan2 709 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸)
32 foeq3 6275 . . . . . . . . . . . . 13 ((𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸 → ((𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸))
3331, 32syl 17 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → ((𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸))
3426, 33mpbid 222 . . . . . . . . . . 11 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸)
35 foco 6287 . . . . . . . . . . 11 ((𝐸:ran 𝐸onto→ω ∧ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸) → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω)
3618, 34, 35sylancr 698 . . . . . . . . . 10 (𝑓:𝐴onto→ω → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω)
37 fowdom 8643 . . . . . . . . . 10 (((𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V ∧ (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω) → ω ≼* (𝑓 “ ran 𝐸))
3823, 36, 37sylancr 698 . . . . . . . . 9 (𝑓:𝐴onto→ω → ω ≼* (𝑓 “ ran 𝐸))
395cnvex 7279 . . . . . . . . . . . 12 𝑓 ∈ V
4039imaex 7270 . . . . . . . . . . 11 (𝑓 “ ran 𝐸) ∈ V
41 isfin3-2 9401 . . . . . . . . . . 11 ((𝑓 “ ran 𝐸) ∈ V → ((𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬ ω ≼* (𝑓 “ ran 𝐸)))
4240, 41ax-mp 5 . . . . . . . . . 10 ((𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬ ω ≼* (𝑓 “ ran 𝐸))
4342con2bii 346 . . . . . . . . 9 (ω ≼* (𝑓 “ ran 𝐸) ↔ ¬ (𝑓 “ ran 𝐸) ∈ FinIII)
4438, 43sylib 208 . . . . . . . 8 (𝑓:𝐴onto→ω → ¬ (𝑓 “ ran 𝐸) ∈ FinIII)
45 fin1a2lem.aa . . . . . . . . . . . . . . 15 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
4614, 45fin1a2lem6 9439 . . . . . . . . . . . . . 14 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)
47 f1ocnv 6311 . . . . . . . . . . . . . 14 ((𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸) → (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran 𝐸)
48 f1ofo 6306 . . . . . . . . . . . . . 14 ((𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran 𝐸(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸)
4946, 47, 48mp2b 10 . . . . . . . . . . . . 13 (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸
50 foco 6287 . . . . . . . . . . . . 13 ((𝐸:ran 𝐸onto→ω ∧ (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) → (𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω)
5118, 49, 50mp2an 710 . . . . . . . . . . . 12 (𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω
52 fofun 6278 . . . . . . . . . . . 12 ((𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω → Fun (𝐸(𝑆 ↾ ran 𝐸)))
5351, 52ax-mp 5 . . . . . . . . . . 11 Fun (𝐸(𝑆 ↾ ran 𝐸))
545resex 5601 . . . . . . . . . . 11 (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))) ∈ V
55 cofunexg 7296 . . . . . . . . . . 11 ((Fun (𝐸(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))) ∈ V) → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V)
5653, 54, 55mp2an 710 . . . . . . . . . 10 ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V
57 difss 3880 . . . . . . . . . . . . . 14 (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ 𝐴
5857, 11syl5sseqr 3795 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ dom 𝑓)
59 fores 6286 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
6024, 58, 59syl2anc 696 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
61 funcnvcnv 6117 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → Fun 𝑓)
62 imadif 6134 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 “ (ω ∖ ran 𝐸)) = ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)))
6324, 61, 623syl 18 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto→ω → (𝑓 “ (ω ∖ ran 𝐸)) = ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)))
6463imaeq2d 5624 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸))))
65 difss 3880 . . . . . . . . . . . . . . 15 (ω ∖ ran 𝐸) ⊆ ω
66 foimacnv 6316 . . . . . . . . . . . . . . 15 ((𝑓:𝐴onto→ω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
6765, 66mpan2 709 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
68 fimacnv 6511 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴⟶ω → (𝑓 “ ω) = 𝐴)
696, 68syl 17 . . . . . . . . . . . . . . . 16 (𝑓:𝐴onto→ω → (𝑓 “ ω) = 𝐴)
7069difeq1d 3870 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto→ω → ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)) = (𝐴 ∖ (𝑓 “ ran 𝐸)))
7170imaeq2d 5624 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
7264, 67, 713eqtr3rd 2803 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸))
73 foeq3 6275 . . . . . . . . . . . . 13 ((𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸) → ((𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)))
7472, 73syl 17 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → ((𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)))
7560, 74mpbid 222 . . . . . . . . . . 11 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))
76 foco 6287 . . . . . . . . . . 11 (((𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω ∧ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω)
7751, 75, 76sylancr 698 . . . . . . . . . 10 (𝑓:𝐴onto→ω → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω)
78 fowdom 8643 . . . . . . . . . 10 ((((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V ∧ ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω) → ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)))
7956, 77, 78sylancr 698 . . . . . . . . 9 (𝑓:𝐴onto→ω → ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)))
80 difexg 4960 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ V)
81 isfin3-2 9401 . . . . . . . . . . 11 ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬ ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸))))
828, 80, 813syl 18 . . . . . . . . . 10 (𝑓:𝐴onto→ω → ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬ ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸))))
8382con2bid 343 . . . . . . . . 9 (𝑓:𝐴onto→ω → (ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
8479, 83mpbid 222 . . . . . . . 8 (𝑓:𝐴onto→ω → ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)
85 eleq1 2827 . . . . . . . . . . . 12 (𝑦 = (𝑓 “ ran 𝐸) → (𝑦 ∈ FinIII ↔ (𝑓 “ ran 𝐸) ∈ FinIII))
86 difeq2 3865 . . . . . . . . . . . . 13 (𝑦 = (𝑓 “ ran 𝐸) → (𝐴𝑦) = (𝐴 ∖ (𝑓 “ ran 𝐸)))
8786eleq1d 2824 . . . . . . . . . . . 12 (𝑦 = (𝑓 “ ran 𝐸) → ((𝐴𝑦) ∈ FinIII ↔ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
8885, 87orbi12d 748 . . . . . . . . . . 11 (𝑦 = (𝑓 “ ran 𝐸) → ((𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
8988notbid 307 . . . . . . . . . 10 (𝑦 = (𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ¬ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
90 ioran 512 . . . . . . . . . 10 (¬ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII) ↔ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
9189, 90syl6bb 276 . . . . . . . . 9 (𝑦 = (𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
9291rspcev 3449 . . . . . . . 8 (((𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)) → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9313, 44, 84, 92syl12anc 1475 . . . . . . 7 (𝑓:𝐴onto→ω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
94 rexnal 3133 . . . . . . 7 (∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9593, 94sylib 208 . . . . . 6 (𝑓:𝐴onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9695exlimiv 2007 . . . . 5 (∃𝑓 𝑓:𝐴onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
974, 96sylbi 207 . . . 4 (ω ≼* 𝐴 → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9897con2i 134 . . 3 (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) → ¬ ω ≼* 𝐴)
99 isfin3-2 9401 . . 3 (𝐴𝑉 → (𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴))
10098, 99syl5ibr 236 . 2 (𝐴𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) → 𝐴 ∈ FinIII))
101100imp 444 1 ((𝐴𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII)) → 𝐴 ∈ FinIII)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  cdif 3712  wss 3715  c0 4058  𝒫 cpw 4302   class class class wbr 4804  cmpt 4881  ccnv 5265  dom cdm 5266  ran crn 5267  cres 5268  cima 5269  ccom 5270  Oncon0 5884  suc csuc 5886  Fun wfun 6043  wf 6045  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  (class class class)co 6814  ωcom 7231  2𝑜c2o 7724   ·𝑜 comu 7728  * cwdom 8629  FinIIIcfin3 9315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-seqom 7713  df-1o 7730  df-2o 7731  df-oadd 7734  df-omul 7735  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-wdom 8631  df-card 8975  df-fin4 9321  df-fin3 9322
This theorem is referenced by:  fin1a2lem8  9441
  Copyright terms: Public domain W3C validator