Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1137 Structured version   Visualization version   GIF version

Theorem bnj1137 33274
Description: Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
Hypothesis
Ref Expression
bnj1137.1 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
Assertion
Ref Expression
bnj1137 ((𝑅 FrSe 𝐴𝑋𝐴) → TrFo(𝐵, 𝐴, 𝑅))
Distinct variable groups:   𝑦,𝐴   𝑦,𝑅   𝑦,𝑋
Allowed substitution hint:   𝐵(𝑦)

Proof of Theorem bnj1137
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 bnj1137.1 . . . . . 6 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
21eleq2i 2828 . . . . 5 (𝑣𝐵𝑣 ∈ ( pred(𝑋, 𝐴, 𝑅) ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
3 elun 4096 . . . . 5 (𝑣 ∈ ( pred(𝑋, 𝐴, 𝑅) ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ↔ (𝑣 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
42, 3bitri 274 . . . 4 (𝑣𝐵 ↔ (𝑣 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
5 bnj213 33161 . . . . . . . . 9 pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
65sseli 3928 . . . . . . . 8 (𝑣 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑣𝐴)
7 bnj906 33209 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝑣𝐴) → pred(𝑣, 𝐴, 𝑅) ⊆ trCl(𝑣, 𝐴, 𝑅))
87adantlr 712 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣𝐴) → pred(𝑣, 𝐴, 𝑅) ⊆ trCl(𝑣, 𝐴, 𝑅))
96, 8sylan2 593 . . . . . . 7 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑣, 𝐴, 𝑅) ⊆ trCl(𝑣, 𝐴, 𝑅))
10 bnj906 33209 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝑋𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
1110sselda 3932 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑣 ∈ trCl(𝑋, 𝐴, 𝑅))
12 bnj18eq1 33206 . . . . . . . . 9 (𝑦 = 𝑣 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑣, 𝐴, 𝑅))
1312ssiun2s 4996 . . . . . . . 8 (𝑣 ∈ trCl(𝑋, 𝐴, 𝑅) → trCl(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
1411, 13syl 17 . . . . . . 7 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
159, 14sstrd 3942 . . . . . 6 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
16 bnj1147 33273 . . . . . . . . . . 11 trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
1716rgenw 3065 . . . . . . . . . 10 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
18 iunss 4993 . . . . . . . . . 10 ( 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴 ↔ ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴)
1917, 18mpbir 230 . . . . . . . . 9 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
2019sseli 3928 . . . . . . . 8 (𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → 𝑣𝐴)
2120, 8sylan2 593 . . . . . . 7 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑣, 𝐴, 𝑅) ⊆ trCl(𝑣, 𝐴, 𝑅))
22 bnj1125 33271 . . . . . . . . . . . 12 ((𝑅 FrSe 𝐴𝑋𝐴𝑦 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
23223expia 1120 . . . . . . . . . . 11 ((𝑅 FrSe 𝐴𝑋𝐴) → (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)))
2423ralrimiv 3138 . . . . . . . . . 10 ((𝑅 FrSe 𝐴𝑋𝐴) → ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
25 iunss 4993 . . . . . . . . . 10 ( 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) ↔ ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
2624, 25sylibr 233 . . . . . . . . 9 ((𝑅 FrSe 𝐴𝑋𝐴) → 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
2726sselda 3932 . . . . . . . 8 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑣 ∈ trCl(𝑋, 𝐴, 𝑅))
2827, 13syl 17 . . . . . . 7 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
2921, 28sstrd 3942 . . . . . 6 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
3015, 29jaodan 955 . . . . 5 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ (𝑣 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))) → pred(𝑣, 𝐴, 𝑅) ⊆ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
31 ssun2 4121 . . . . . 6 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
3231, 1sseqtrri 3969 . . . . 5 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵
3330, 32sstrdi 3944 . . . 4 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ (𝑣 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑣 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))) → pred(𝑣, 𝐴, 𝑅) ⊆ 𝐵)
344, 33sylan2b 594 . . 3 (((𝑅 FrSe 𝐴𝑋𝐴) ∧ 𝑣𝐵) → pred(𝑣, 𝐴, 𝑅) ⊆ 𝐵)
3534ralrimiva 3139 . 2 ((𝑅 FrSe 𝐴𝑋𝐴) → ∀𝑣𝐵 pred(𝑣, 𝐴, 𝑅) ⊆ 𝐵)
36 df-bnj19 32976 . 2 ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑣𝐵 pred(𝑣, 𝐴, 𝑅) ⊆ 𝐵)
3735, 36sylibr 233 1 ((𝑅 FrSe 𝐴𝑋𝐴) → TrFo(𝐵, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 844   = wceq 1540  wcel 2105  wral 3061  cun 3896  wss 3898   ciun 4942   predc-bnj14 32967   FrSe w-bnj15 32971   trClc-bnj18 32973   TrFow-bnj19 32975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-reg 9450  ax-inf2 9499
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-om 7782  df-1o 8368  df-bnj17 32966  df-bnj14 32968  df-bnj13 32970  df-bnj15 32972  df-bnj18 32974  df-bnj19 32976
This theorem is referenced by:  bnj1136  33276
  Copyright terms: Public domain W3C validator