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

Theorem fin23lem12 9440
Description: The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets).

This first section is dedicated to the construction of 𝑈 and its intersection. First, the value of 𝑈 at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)

Hypothesis
Ref Expression
fin23lem.a 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢))), ran 𝑡)
Assertion
Ref Expression
fin23lem12 (𝐴 ∈ ω → (𝑈‘suc 𝐴) = if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))))
Distinct variable groups:   𝑡,𝑖,𝑢   𝐴,𝑖,𝑢   𝑈,𝑖,𝑢
Allowed substitution hints:   𝐴(𝑡)   𝑈(𝑡)

Proof of Theorem fin23lem12
StepHypRef Expression
1 fin23lem.a . . 3 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢))), ran 𝑡)
21seqomsuc 7790 . 2 (𝐴 ∈ ω → (𝑈‘suc 𝐴) = (𝐴(𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢)))(𝑈𝐴)))
3 fvex 6423 . . 3 (𝑈𝐴) ∈ V
4 fveq2 6410 . . . . . . 7 (𝑖 = 𝐴 → (𝑡𝑖) = (𝑡𝐴))
54ineq1d 4010 . . . . . 6 (𝑖 = 𝐴 → ((𝑡𝑖) ∩ 𝑢) = ((𝑡𝐴) ∩ 𝑢))
65eqeq1d 2800 . . . . 5 (𝑖 = 𝐴 → (((𝑡𝑖) ∩ 𝑢) = ∅ ↔ ((𝑡𝐴) ∩ 𝑢) = ∅))
76, 5ifbieq2d 4301 . . . 4 (𝑖 = 𝐴 → if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢)) = if(((𝑡𝐴) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝐴) ∩ 𝑢)))
8 ineq2 4005 . . . . . 6 (𝑢 = (𝑈𝐴) → ((𝑡𝐴) ∩ 𝑢) = ((𝑡𝐴) ∩ (𝑈𝐴)))
98eqeq1d 2800 . . . . 5 (𝑢 = (𝑈𝐴) → (((𝑡𝐴) ∩ 𝑢) = ∅ ↔ ((𝑡𝐴) ∩ (𝑈𝐴)) = ∅))
10 id 22 . . . . 5 (𝑢 = (𝑈𝐴) → 𝑢 = (𝑈𝐴))
119, 10, 8ifbieq12d 4303 . . . 4 (𝑢 = (𝑈𝐴) → if(((𝑡𝐴) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝐴) ∩ 𝑢)) = if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))))
12 eqid 2798 . . . 4 (𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢))) = (𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢)))
133inex2 4994 . . . . 5 ((𝑡𝐴) ∩ (𝑈𝐴)) ∈ V
143, 13ifex 4324 . . . 4 if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))) ∈ V
157, 11, 12, 14ovmpt2 7029 . . 3 ((𝐴 ∈ ω ∧ (𝑈𝐴) ∈ V) → (𝐴(𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢)))(𝑈𝐴)) = if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))))
163, 15mpan2 683 . 2 (𝐴 ∈ ω → (𝐴(𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢)))(𝑈𝐴)) = if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))))
172, 16eqtrd 2832 1 (𝐴 ∈ ω → (𝑈‘suc 𝐴) = if(((𝑡𝐴) ∩ (𝑈𝐴)) = ∅, (𝑈𝐴), ((𝑡𝐴) ∩ (𝑈𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  Vcvv 3384  cin 3767  c0 4114  ifcif 4276   cuni 4627  ran crn 5312  suc csuc 5942  cfv 6100  (class class class)co 6877  cmpt2 6879  ωcom 7298  seq𝜔cseqom 7780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-2nd 7401  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-seqom 7781
This theorem is referenced by:  fin23lem13  9441  fin23lem14  9442  fin23lem19  9445
  Copyright terms: Public domain W3C validator