Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  smores Structured version   GIF version

Theorem smores 5848
 Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
Assertion
Ref Expression
smores ((Smo A B dom A) → Smo (AB))

Proof of Theorem smores
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funres 4884 . . . . . . . 8 (Fun A → Fun (AB))
2 funfn 4874 . . . . . . . 8 (Fun AA Fn dom A)
3 funfn 4874 . . . . . . . 8 (Fun (AB) ↔ (AB) Fn dom (AB))
41, 2, 33imtr3i 189 . . . . . . 7 (A Fn dom A → (AB) Fn dom (AB))
5 resss 4578 . . . . . . . . 9 (AB) ⊆ A
6 rnss 4507 . . . . . . . . 9 ((AB) ⊆ A → ran (AB) ⊆ ran A)
75, 6ax-mp 7 . . . . . . . 8 ran (AB) ⊆ ran A
8 sstr 2947 . . . . . . . 8 ((ran (AB) ⊆ ran A ran A ⊆ On) → ran (AB) ⊆ On)
97, 8mpan 400 . . . . . . 7 (ran A ⊆ On → ran (AB) ⊆ On)
104, 9anim12i 321 . . . . . 6 ((A Fn dom A ran A ⊆ On) → ((AB) Fn dom (AB) ran (AB) ⊆ On))
11 df-f 4849 . . . . . 6 (A:dom A⟶On ↔ (A Fn dom A ran A ⊆ On))
12 df-f 4849 . . . . . 6 ((AB):dom (AB)⟶On ↔ ((AB) Fn dom (AB) ran (AB) ⊆ On))
1310, 11, 123imtr4i 190 . . . . 5 (A:dom A⟶On → (AB):dom (AB)⟶On)
1413a1i 9 . . . 4 (B dom A → (A:dom A⟶On → (AB):dom (AB)⟶On))
15 ordelord 4084 . . . . . . 7 ((Ord dom A B dom A) → Ord B)
1615expcom 109 . . . . . 6 (B dom A → (Ord dom A → Ord B))
17 ordin 4088 . . . . . . 7 ((Ord B Ord dom A) → Ord (B ∩ dom A))
1817ex 108 . . . . . 6 (Ord B → (Ord dom A → Ord (B ∩ dom A)))
1916, 18syli 33 . . . . 5 (B dom A → (Ord dom A → Ord (B ∩ dom A)))
20 dmres 4575 . . . . . 6 dom (AB) = (B ∩ dom A)
21 ordeq 4075 . . . . . 6 (dom (AB) = (B ∩ dom A) → (Ord dom (AB) ↔ Ord (B ∩ dom A)))
2220, 21ax-mp 7 . . . . 5 (Ord dom (AB) ↔ Ord (B ∩ dom A))
2319, 22syl6ibr 151 . . . 4 (B dom A → (Ord dom A → Ord dom (AB)))
24 dmss 4477 . . . . . . . . 9 ((AB) ⊆ A → dom (AB) ⊆ dom A)
255, 24ax-mp 7 . . . . . . . 8 dom (AB) ⊆ dom A
26 ssralv 2998 . . . . . . . 8 (dom (AB) ⊆ dom A → (x dom Ay dom A(x y → (Ax) (Ay)) → x dom (AB)y dom A(x y → (Ax) (Ay))))
2725, 26ax-mp 7 . . . . . . 7 (x dom Ay dom A(x y → (Ax) (Ay)) → x dom (AB)y dom A(x y → (Ax) (Ay)))
28 ssralv 2998 . . . . . . . . 9 (dom (AB) ⊆ dom A → (y dom A(x y → (Ax) (Ay)) → y dom (AB)(x y → (Ax) (Ay))))
2925, 28ax-mp 7 . . . . . . . 8 (y dom A(x y → (Ax) (Ay)) → y dom (AB)(x y → (Ax) (Ay)))
3029ralimi 2378 . . . . . . 7 (x dom (AB)y dom A(x y → (Ax) (Ay)) → x dom (AB)y dom (AB)(x y → (Ax) (Ay)))
3127, 30syl 14 . . . . . 6 (x dom Ay dom A(x y → (Ax) (Ay)) → x dom (AB)y dom (AB)(x y → (Ax) (Ay)))
32 inss1 3151 . . . . . . . . . . . . 13 (B ∩ dom A) ⊆ B
3320, 32eqsstri 2969 . . . . . . . . . . . 12 dom (AB) ⊆ B
34 simpl 102 . . . . . . . . . . . 12 ((x dom (AB) y dom (AB)) → x dom (AB))
3533, 34sseldi 2937 . . . . . . . . . . 11 ((x dom (AB) y dom (AB)) → x B)
36 fvres 5141 . . . . . . . . . . 11 (x B → ((AB)‘x) = (Ax))
3735, 36syl 14 . . . . . . . . . 10 ((x dom (AB) y dom (AB)) → ((AB)‘x) = (Ax))
38 simpr 103 . . . . . . . . . . . 12 ((x dom (AB) y dom (AB)) → y dom (AB))
3933, 38sseldi 2937 . . . . . . . . . . 11 ((x dom (AB) y dom (AB)) → y B)
40 fvres 5141 . . . . . . . . . . 11 (y B → ((AB)‘y) = (Ay))
4139, 40syl 14 . . . . . . . . . 10 ((x dom (AB) y dom (AB)) → ((AB)‘y) = (Ay))
4237, 41eleq12d 2105 . . . . . . . . 9 ((x dom (AB) y dom (AB)) → (((AB)‘x) ((AB)‘y) ↔ (Ax) (Ay)))
4342imbi2d 219 . . . . . . . 8 ((x dom (AB) y dom (AB)) → ((x y → ((AB)‘x) ((AB)‘y)) ↔ (x y → (Ax) (Ay))))
4443ralbidva 2316 . . . . . . 7 (x dom (AB) → (y dom (AB)(x y → ((AB)‘x) ((AB)‘y)) ↔ y dom (AB)(x y → (Ax) (Ay))))
4544ralbiia 2332 . . . . . 6 (x dom (AB)y dom (AB)(x y → ((AB)‘x) ((AB)‘y)) ↔ x dom (AB)y dom (AB)(x y → (Ax) (Ay)))
4631, 45sylibr 137 . . . . 5 (x dom Ay dom A(x y → (Ax) (Ay)) → x dom (AB)y dom (AB)(x y → ((AB)‘x) ((AB)‘y)))
4746a1i 9 . . . 4 (B dom A → (x dom Ay dom A(x y → (Ax) (Ay)) → x dom (AB)y dom (AB)(x y → ((AB)‘x) ((AB)‘y))))
4814, 23, 473anim123d 1213 . . 3 (B dom A → ((A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay))) → ((AB):dom (AB)⟶On Ord dom (AB) x dom (AB)y dom (AB)(x y → ((AB)‘x) ((AB)‘y)))))
49 df-smo 5842 . . 3 (Smo A ↔ (A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay))))
50 df-smo 5842 . . 3 (Smo (AB) ↔ ((AB):dom (AB)⟶On Ord dom (AB) x dom (AB)y dom (AB)(x y → ((AB)‘x) ((AB)‘y))))
5148, 49, 503imtr4g 194 . 2 (B dom A → (Smo A → Smo (AB)))
5251impcom 116 1 ((Smo A B dom A) → Smo (AB))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300   ∩ cin 2910   ⊆ wss 2911  Ord word 4065  Oncon0 4066  dom cdm 4288  ran crn 4289   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ⟶wf 4841  ‘cfv 4845  Smo wsmo 5841 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935 This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-tr 3846  df-iord 4069  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853  df-smo 5842 This theorem is referenced by:  smores3  5849
 Copyright terms: Public domain W3C validator