Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erdszelem1 Structured version   Visualization version   GIF version

Theorem erdszelem1 34858
Description: Lemma for erdsze 34869. (Contributed by Mario Carneiro, 22-Jan-2015.)
Hypothesis
Ref Expression
erdszelem1.1 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
Assertion
Ref Expression
erdszelem1 (𝑋𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹   𝑦,𝑂   𝑦,𝑋
Allowed substitution hint:   𝑆(𝑦)

Proof of Theorem erdszelem1
StepHypRef Expression
1 ovex 7449 . . . 4 (1...𝐴) ∈ V
21elpw2 5342 . . 3 (𝑋 ∈ 𝒫 (1...𝐴) ↔ 𝑋 ⊆ (1...𝐴))
32anbi1i 622 . 2 ((𝑋 ∈ 𝒫 (1...𝐴) ∧ ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋)) ↔ (𝑋 ⊆ (1...𝐴) ∧ ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋)))
4 reseq2 5974 . . . . . 6 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
5 isoeq1 7321 . . . . . 6 ((𝐹𝑦) = (𝐹𝑋) → ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑦, (𝐹𝑦))))
64, 5syl 17 . . . . 5 (𝑦 = 𝑋 → ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑦, (𝐹𝑦))))
7 isoeq4 7324 . . . . 5 (𝑦 = 𝑋 → ((𝐹𝑋) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑦))))
8 imaeq2 6054 . . . . . 6 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
9 isoeq5 7325 . . . . . 6 ((𝐹𝑦) = (𝐹𝑋) → ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋))))
108, 9syl 17 . . . . 5 (𝑦 = 𝑋 → ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋))))
116, 7, 103bitrd 304 . . . 4 (𝑦 = 𝑋 → ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ↔ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋))))
12 eleq2 2814 . . . 4 (𝑦 = 𝑋 → (𝐴𝑦𝐴𝑋))
1311, 12anbi12d 630 . . 3 (𝑦 = 𝑋 → (((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦) ↔ ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋)))
14 erdszelem1.1 . . 3 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1513, 14elrab2 3677 . 2 (𝑋𝑆 ↔ (𝑋 ∈ 𝒫 (1...𝐴) ∧ ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋)))
16 3anass 1092 . 2 ((𝑋 ⊆ (1...𝐴) ∧ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋) ↔ (𝑋 ⊆ (1...𝐴) ∧ ((𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋)))
173, 15, 163bitr4i 302 1 (𝑋𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹𝑋) Isom < , 𝑂 (𝑋, (𝐹𝑋)) ∧ 𝐴𝑋))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  {crab 3419  wss 3939  𝒫 cpw 4598  cres 5674  cima 5675   Isom wiso 6544  (class class class)co 7416  1c1 11139   < clt 11278  ...cfz 13516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5294  ax-nul 5301
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5144  df-opab 5206  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-ov 7419
This theorem is referenced by:  erdszelem2  34859  erdszelem4  34861  erdszelem7  34864  erdszelem8  34865
  Copyright terms: Public domain W3C validator