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

Theorem fin1a2lem12 9914
Description: Lemma for fin1a2 9918. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
fin1a2lem12 (((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ FinIII)

Proof of Theorem fin1a2lem12
Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 488 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → 𝐵 ∈ FinIII)
2 simpll1 1213 . . . . . . 7 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → 𝐴 ⊆ 𝒫 𝐵)
32adantr 484 . . . . . 6 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4 ssrab2 3970 . . . . . . . 8 {𝑓𝐴𝑓𝑒} ⊆ 𝐴
54unissi 4806 . . . . . . 7 {𝑓𝐴𝑓𝑒} ⊆ 𝐴
6 sspwuni 4986 . . . . . . . 8 (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)
76biimpi 219 . . . . . . 7 (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)
85, 7sstrid 3889 . . . . . 6 (𝐴 ⊆ 𝒫 𝐵 {𝑓𝐴𝑓𝑒} ⊆ 𝐵)
93, 8syl 17 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑒 ∈ ω) → {𝑓𝐴𝑓𝑒} ⊆ 𝐵)
10 elpw2g 5213 . . . . . 6 (𝐵 ∈ FinIII → ( {𝑓𝐴𝑓𝑒} ∈ 𝒫 𝐵 {𝑓𝐴𝑓𝑒} ⊆ 𝐵))
1110ad2antlr 727 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑒 ∈ ω) → ( {𝑓𝐴𝑓𝑒} ∈ 𝒫 𝐵 {𝑓𝐴𝑓𝑒} ⊆ 𝐵))
129, 11mpbird 260 . . . 4 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑒 ∈ ω) → {𝑓𝐴𝑓𝑒} ∈ 𝒫 𝐵)
1312fmpttd 6892 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}):ω⟶𝒫 𝐵)
14 vex 3403 . . . . . . . . . . 11 𝑑 ∈ V
1514sucex 7548 . . . . . . . . . 10 suc 𝑑 ∈ V
16 sssucid 6250 . . . . . . . . . 10 𝑑 ⊆ suc 𝑑
17 ssdomg 8604 . . . . . . . . . 10 (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑𝑑 ≼ suc 𝑑))
1815, 16, 17mp2 9 . . . . . . . . 9 𝑑 ≼ suc 𝑑
19 domtr 8611 . . . . . . . . 9 ((𝑓𝑑𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
2018, 19mpan2 691 . . . . . . . 8 (𝑓𝑑𝑓 ≼ suc 𝑑)
2120a1i 11 . . . . . . 7 (𝑓𝐴 → (𝑓𝑑𝑓 ≼ suc 𝑑))
2221ss2rabi 3967 . . . . . 6 {𝑓𝐴𝑓𝑑} ⊆ {𝑓𝐴𝑓 ≼ suc 𝑑}
23 uniss 4805 . . . . . 6 ({𝑓𝐴𝑓𝑑} ⊆ {𝑓𝐴𝑓 ≼ suc 𝑑} → {𝑓𝐴𝑓𝑑} ⊆ {𝑓𝐴𝑓 ≼ suc 𝑑})
2422, 23mp1i 13 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑑 ∈ ω) → {𝑓𝐴𝑓𝑑} ⊆ {𝑓𝐴𝑓 ≼ suc 𝑑})
25 id 22 . . . . . 6 (𝑑 ∈ ω → 𝑑 ∈ ω)
26 pwexg 5246 . . . . . . . . 9 (𝐵 ∈ FinIII → 𝒫 𝐵 ∈ V)
2726adantl 485 . . . . . . . 8 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → 𝒫 𝐵 ∈ V)
2827, 2ssexd 5193 . . . . . . 7 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → 𝐴 ∈ V)
29 rabexg 5200 . . . . . . 7 (𝐴 ∈ V → {𝑓𝐴𝑓𝑑} ∈ V)
30 uniexg 7487 . . . . . . 7 ({𝑓𝐴𝑓𝑑} ∈ V → {𝑓𝐴𝑓𝑑} ∈ V)
3128, 29, 303syl 18 . . . . . 6 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → {𝑓𝐴𝑓𝑑} ∈ V)
32 breq2 5035 . . . . . . . . 9 (𝑒 = 𝑑 → (𝑓𝑒𝑓𝑑))
3332rabbidv 3382 . . . . . . . 8 (𝑒 = 𝑑 → {𝑓𝐴𝑓𝑒} = {𝑓𝐴𝑓𝑑})
3433unieqd 4811 . . . . . . 7 (𝑒 = 𝑑 {𝑓𝐴𝑓𝑒} = {𝑓𝐴𝑓𝑑})
35 eqid 2739 . . . . . . 7 (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})
3634, 35fvmptg 6776 . . . . . 6 ((𝑑 ∈ ω ∧ {𝑓𝐴𝑓𝑑} ∈ V) → ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘𝑑) = {𝑓𝐴𝑓𝑑})
3725, 31, 36syl2anr 600 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘𝑑) = {𝑓𝐴𝑓𝑑})
38 peano2 7624 . . . . . 6 (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39 rabexg 5200 . . . . . . 7 (𝐴 ∈ V → {𝑓𝐴𝑓 ≼ suc 𝑑} ∈ V)
40 uniexg 7487 . . . . . . 7 ({𝑓𝐴𝑓 ≼ suc 𝑑} ∈ V → {𝑓𝐴𝑓 ≼ suc 𝑑} ∈ V)
4128, 39, 403syl 18 . . . . . 6 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → {𝑓𝐴𝑓 ≼ suc 𝑑} ∈ V)
42 breq2 5035 . . . . . . . . 9 (𝑒 = suc 𝑑 → (𝑓𝑒𝑓 ≼ suc 𝑑))
4342rabbidv 3382 . . . . . . . 8 (𝑒 = suc 𝑑 → {𝑓𝐴𝑓𝑒} = {𝑓𝐴𝑓 ≼ suc 𝑑})
4443unieqd 4811 . . . . . . 7 (𝑒 = suc 𝑑 {𝑓𝐴𝑓𝑒} = {𝑓𝐴𝑓 ≼ suc 𝑑})
4544, 35fvmptg 6776 . . . . . 6 ((suc 𝑑 ∈ ω ∧ {𝑓𝐴𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘suc 𝑑) = {𝑓𝐴𝑓 ≼ suc 𝑑})
4638, 41, 45syl2anr 600 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘suc 𝑑) = {𝑓𝐴𝑓 ≼ suc 𝑑})
4724, 37, 463sstr4d 3925 . . . 4 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘suc 𝑑))
4847ralrimiva 3097 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘suc 𝑑))
49 fin34i 9884 . . 3 ((𝐵 ∈ FinIII ∧ (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})‘suc 𝑑)) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}))
501, 13, 48, 49syl3anc 1372 . 2 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}))
51 fin1a2lem11 9913 . . . . . 6 (( [] Or 𝐴𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
5251adantrr 717 . . . . 5 (( [] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
53523ad2antl2 1187 . . . 4 (((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
5453adantr 484 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
55 simpll3 1215 . . . . . 6 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ¬ 𝐴𝐴)
56 simplrr 778 . . . . . . 7 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → 𝐴 ≠ ∅)
57 sspwuni 4986 . . . . . . . . . . 11 (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ ∅)
58 ss0b 4287 . . . . . . . . . . 11 ( 𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
5957, 58bitri 278 . . . . . . . . . 10 (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 = ∅)
60 pw0 4701 . . . . . . . . . . . . 13 𝒫 ∅ = {∅}
6160sseq2i 3907 . . . . . . . . . . . 12 (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62 sssn 4715 . . . . . . . . . . . 12 (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
6361, 62bitri 278 . . . . . . . . . . 11 (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64 df-ne 2936 . . . . . . . . . . . 12 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65 0ex 5176 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
6665unisn 4819 . . . . . . . . . . . . . . . 16 {∅} = ∅
6765snid 4553 . . . . . . . . . . . . . . . 16 ∅ ∈ {∅}
6866, 67eqeltri 2830 . . . . . . . . . . . . . . 15 {∅} ∈ {∅}
69 unieq 4808 . . . . . . . . . . . . . . . 16 (𝐴 = {∅} → 𝐴 = {∅})
70 id 22 . . . . . . . . . . . . . . . 16 (𝐴 = {∅} → 𝐴 = {∅})
7169, 70eleq12d 2828 . . . . . . . . . . . . . . 15 (𝐴 = {∅} → ( 𝐴𝐴 {∅} ∈ {∅}))
7268, 71mpbiri 261 . . . . . . . . . . . . . 14 (𝐴 = {∅} → 𝐴𝐴)
7372orim2i 910 . . . . . . . . . . . . 13 ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ 𝐴𝐴))
7473ord 863 . . . . . . . . . . . 12 ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → 𝐴𝐴))
7564, 74syl5bi 245 . . . . . . . . . . 11 ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → 𝐴𝐴))
7663, 75sylbi 220 . . . . . . . . . 10 (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → 𝐴𝐴))
7759, 76sylbir 238 . . . . . . . . 9 ( 𝐴 = ∅ → (𝐴 ≠ ∅ → 𝐴𝐴))
7877com12 32 . . . . . . . 8 (𝐴 ≠ ∅ → ( 𝐴 = ∅ → 𝐴𝐴))
7978con3d 155 . . . . . . 7 (𝐴 ≠ ∅ → (¬ 𝐴𝐴 → ¬ 𝐴 = ∅))
8056, 55, 79sylc 65 . . . . . 6 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ¬ 𝐴 = ∅)
81 ioran 983 . . . . . 6 (¬ ( 𝐴𝐴 𝐴 = ∅) ↔ (¬ 𝐴𝐴 ∧ ¬ 𝐴 = ∅))
8255, 80, 81sylanbrc 586 . . . . 5 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ¬ ( 𝐴𝐴 𝐴 = ∅))
83 uniun 4822 . . . . . . . 8 (𝐴 ∪ {∅}) = ( 𝐴 {∅})
8466uneq2i 4051 . . . . . . . 8 ( 𝐴 {∅}) = ( 𝐴 ∪ ∅)
85 un0 4280 . . . . . . . 8 ( 𝐴 ∪ ∅) = 𝐴
8683, 84, 853eqtri 2766 . . . . . . 7 (𝐴 ∪ {∅}) = 𝐴
8786eleq1i 2824 . . . . . 6 ( (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ 𝐴 ∈ (𝐴 ∪ {∅}))
88 elun 4040 . . . . . 6 ( 𝐴 ∈ (𝐴 ∪ {∅}) ↔ ( 𝐴𝐴 𝐴 ∈ {∅}))
8965elsn2 4556 . . . . . . 7 ( 𝐴 ∈ {∅} ↔ 𝐴 = ∅)
9089orbi2i 912 . . . . . 6 (( 𝐴𝐴 𝐴 ∈ {∅}) ↔ ( 𝐴𝐴 𝐴 = ∅))
9187, 88, 903bitri 300 . . . . 5 ( (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ( 𝐴𝐴 𝐴 = ∅))
9282, 91sylnibr 332 . . . 4 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ¬ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93 unieq 4808 . . . . . 6 (ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
94 id 22 . . . . . 6 (ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}))
9593, 94eleq12d 2828 . . . . 5 (ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}) → ( ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ↔ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
9695notbid 321 . . . 4 (ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}) → (¬ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ↔ ¬ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
9792, 96syl5ibrcom 250 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → (ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) = (𝐴 ∪ {∅}) → ¬ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒})))
9854, 97mpd 15 . 2 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ FinIII) → ¬ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}) ∈ ran (𝑒 ∈ ω ↦ {𝑓𝐴𝑓𝑒}))
9950, 98pm2.65da 817 1 (((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ FinIII)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wcel 2114  wne 2935  wral 3054  {crab 3058  Vcvv 3399  cun 3842  wss 3844  c0 4212  𝒫 cpw 4489  {csn 4517   cuni 4797   class class class wbr 5031  cmpt 5111   Or wor 5442  ran crn 5527  suc csuc 6175  wf 6336  cfv 6340   [] crpss 7469  ωcom 7602  cdom 8556  Fincfn 8558  FinIIIcfin3 9784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7130  df-rpss 7470  df-om 7603  df-wrecs 7979  df-recs 8040  df-rdg 8078  df-1o 8134  df-er 8323  df-en 8559  df-dom 8560  df-sdom 8561  df-fin 8562  df-wdom 9105  df-card 9444  df-fin4 9790  df-fin3 9791
This theorem is referenced by:  fin1a2s  9917
  Copyright terms: Public domain W3C validator