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

Theorem fpwwe2lem10 10053
Description: Lemma for fpwwe2 10057. Given two well-orders 𝑋, 𝑅 and 𝑌, 𝑆 of parts of 𝐴, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2lem10.4 (𝜑𝑋𝑊𝑅)
fpwwe2lem10.6 (𝜑𝑌𝑊𝑆)
Assertion
Ref Expression
fpwwe2lem10 (𝜑 → ((𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌𝑋𝑆 = (𝑅 ∩ (𝑋 × 𝑌)))))
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem10
StepHypRef Expression
1 eqid 2824 . . . 4 OrdIso(𝑅, 𝑋) = OrdIso(𝑅, 𝑋)
21oicl 8985 . . 3 Ord dom OrdIso(𝑅, 𝑋)
3 eqid 2824 . . . 4 OrdIso(𝑆, 𝑌) = OrdIso(𝑆, 𝑌)
43oicl 8985 . . 3 Ord dom OrdIso(𝑆, 𝑌)
5 ordtri2or2 6284 . . 3 ((Ord dom OrdIso(𝑅, 𝑋) ∧ Ord dom OrdIso(𝑆, 𝑌)) → (dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌) ∨ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)))
62, 4, 5mp2an 688 . 2 (dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌) ∨ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋))
7 fpwwe2.1 . . . . 5 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
8 fpwwe2.2 . . . . . 6 (𝜑𝐴 ∈ V)
98adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) → 𝐴 ∈ V)
10 fpwwe2.3 . . . . . 6 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
1110adantlr 711 . . . . 5 (((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
12 fpwwe2lem10.4 . . . . . 6 (𝜑𝑋𝑊𝑅)
1312adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) → 𝑋𝑊𝑅)
14 fpwwe2lem10.6 . . . . . 6 (𝜑𝑌𝑊𝑆)
1514adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) → 𝑌𝑊𝑆)
16 simpr 485 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) → dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌))
177, 9, 11, 13, 15, 1, 3, 16fpwwe2lem9 10052 . . . 4 ((𝜑 ∧ dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌)) → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
1817ex 413 . . 3 (𝜑 → (dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌) → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))))
198adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → 𝐴 ∈ V)
2010adantlr 711 . . . . 5 (((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
2114adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → 𝑌𝑊𝑆)
2212adantr 481 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → 𝑋𝑊𝑅)
23 simpr 485 . . . . 5 ((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋))
247, 19, 20, 21, 22, 3, 1, 23fpwwe2lem9 10052 . . . 4 ((𝜑 ∧ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → (𝑌𝑋𝑆 = (𝑅 ∩ (𝑋 × 𝑌))))
2524ex 413 . . 3 (𝜑 → (dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋) → (𝑌𝑋𝑆 = (𝑅 ∩ (𝑋 × 𝑌)))))
2618, 25orim12d 960 . 2 (𝜑 → ((dom OrdIso(𝑅, 𝑋) ⊆ dom OrdIso(𝑆, 𝑌) ∨ dom OrdIso(𝑆, 𝑌) ⊆ dom OrdIso(𝑅, 𝑋)) → ((𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌𝑋𝑆 = (𝑅 ∩ (𝑋 × 𝑌))))))
276, 26mpi 20 1 (𝜑 → ((𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌𝑋𝑆 = (𝑅 ∩ (𝑋 × 𝑌)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2106  wral 3142  Vcvv 3499  [wsbc 3775  cin 3938  wss 3939  {csn 4563   class class class wbr 5062  {copab 5124   We wwe 5511   × cxp 5551  ccnv 5552  dom cdm 5553  cima 5556  Ord word 6187  (class class class)co 7151  OrdIsocoi 8965
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 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-wrecs 7941  df-recs 8002  df-oi 8966
This theorem is referenced by:  fpwwe2lem11  10054  fpwwe2lem12  10055  fpwwe2  10057
  Copyright terms: Public domain W3C validator