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

Theorem onfununi 7961
Description: A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of [Enderton] p. 218. (Contributed by Eric Schmidt, 26-May-2009.)
Hypotheses
Ref Expression
onfununi.1 (Lim 𝑦 → (𝐹𝑦) = 𝑥𝑦 (𝐹𝑥))
onfununi.2 ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦))
Assertion
Ref Expression
onfununi ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹 𝑆) = 𝑥𝑆 (𝐹𝑥))
Distinct variable groups:   𝑥,𝑦,𝑆   𝑥,𝐹,𝑦   𝑥,𝑇
Allowed substitution hint:   𝑇(𝑦)

Proof of Theorem onfununi
StepHypRef Expression
1 ssorduni 7480 . . . . . . . . . 10 (𝑆 ⊆ On → Ord 𝑆)
21ad2antrr 725 . . . . . . . . 9 (((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) ∧ 𝑆 ≠ ∅) → Ord 𝑆)
3 nelneq 2914 . . . . . . . . . . . . . . . 16 ((𝑥𝑆 ∧ ¬ 𝑆𝑆) → ¬ 𝑥 = 𝑆)
4 elssuni 4830 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑆𝑥 𝑆)
54adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑥𝑆) → 𝑥 𝑆)
6 ssel 3908 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 ⊆ On → (𝑥𝑆𝑥 ∈ On))
7 eloni 6169 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ On → Ord 𝑥)
86, 7syl6 35 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ⊆ On → (𝑥𝑆 → Ord 𝑥))
98imp 410 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ⊆ On ∧ 𝑥𝑆) → Ord 𝑥)
10 ordsseleq 6188 . . . . . . . . . . . . . . . . . . . . 21 ((Ord 𝑥 ∧ Ord 𝑆) → (𝑥 𝑆 ↔ (𝑥 𝑆𝑥 = 𝑆)))
119, 1, 10syl2an 598 . . . . . . . . . . . . . . . . . . . 20 (((𝑆 ⊆ On ∧ 𝑥𝑆) ∧ 𝑆 ⊆ On) → (𝑥 𝑆 ↔ (𝑥 𝑆𝑥 = 𝑆)))
1211anabss1 665 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ⊆ On ∧ 𝑥𝑆) → (𝑥 𝑆 ↔ (𝑥 𝑆𝑥 = 𝑆)))
135, 12mpbid 235 . . . . . . . . . . . . . . . . . 18 ((𝑆 ⊆ On ∧ 𝑥𝑆) → (𝑥 𝑆𝑥 = 𝑆))
1413ord 861 . . . . . . . . . . . . . . . . 17 ((𝑆 ⊆ On ∧ 𝑥𝑆) → (¬ 𝑥 𝑆𝑥 = 𝑆))
1514con1d 147 . . . . . . . . . . . . . . . 16 ((𝑆 ⊆ On ∧ 𝑥𝑆) → (¬ 𝑥 = 𝑆𝑥 𝑆))
163, 15syl5 34 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ On ∧ 𝑥𝑆) → ((𝑥𝑆 ∧ ¬ 𝑆𝑆) → 𝑥 𝑆))
1716exp4b 434 . . . . . . . . . . . . . 14 (𝑆 ⊆ On → (𝑥𝑆 → (𝑥𝑆 → (¬ 𝑆𝑆𝑥 𝑆))))
1817pm2.43d 53 . . . . . . . . . . . . 13 (𝑆 ⊆ On → (𝑥𝑆 → (¬ 𝑆𝑆𝑥 𝑆)))
1918com23 86 . . . . . . . . . . . 12 (𝑆 ⊆ On → (¬ 𝑆𝑆 → (𝑥𝑆𝑥 𝑆)))
2019imp 410 . . . . . . . . . . 11 ((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) → (𝑥𝑆𝑥 𝑆))
2120ssrdv 3921 . . . . . . . . . 10 ((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) → 𝑆 𝑆)
22 ssn0 4308 . . . . . . . . . 10 ((𝑆 𝑆𝑆 ≠ ∅) → 𝑆 ≠ ∅)
2321, 22sylan 583 . . . . . . . . 9 (((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) ∧ 𝑆 ≠ ∅) → 𝑆 ≠ ∅)
2421unissd 4810 . . . . . . . . . . 11 ((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) → 𝑆 𝑆)
25 orduniss 6253 . . . . . . . . . . . . 13 (Ord 𝑆 𝑆 𝑆)
261, 25syl 17 . . . . . . . . . . . 12 (𝑆 ⊆ On → 𝑆 𝑆)
2726adantr 484 . . . . . . . . . . 11 ((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) → 𝑆 𝑆)
2824, 27eqssd 3932 . . . . . . . . . 10 ((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) → 𝑆 = 𝑆)
2928adantr 484 . . . . . . . . 9 (((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) ∧ 𝑆 ≠ ∅) → 𝑆 = 𝑆)
30 df-lim 6164 . . . . . . . . 9 (Lim 𝑆 ↔ (Ord 𝑆 𝑆 ≠ ∅ ∧ 𝑆 = 𝑆))
312, 23, 29, 30syl3anbrc 1340 . . . . . . . 8 (((𝑆 ⊆ On ∧ ¬ 𝑆𝑆) ∧ 𝑆 ≠ ∅) → Lim 𝑆)
3231an32s 651 . . . . . . 7 (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → Lim 𝑆)
33323adantl1 1163 . . . . . 6 (((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → Lim 𝑆)
34 ssonuni 7481 . . . . . . . . . 10 (𝑆𝑇 → (𝑆 ⊆ On → 𝑆 ∈ On))
35 limeq 6171 . . . . . . . . . . . 12 (𝑦 = 𝑆 → (Lim 𝑦 ↔ Lim 𝑆))
36 fveq2 6645 . . . . . . . . . . . . 13 (𝑦 = 𝑆 → (𝐹𝑦) = (𝐹 𝑆))
37 iuneq1 4897 . . . . . . . . . . . . 13 (𝑦 = 𝑆 𝑥𝑦 (𝐹𝑥) = 𝑥 𝑆(𝐹𝑥))
3836, 37eqeq12d 2814 . . . . . . . . . . . 12 (𝑦 = 𝑆 → ((𝐹𝑦) = 𝑥𝑦 (𝐹𝑥) ↔ (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥)))
3935, 38imbi12d 348 . . . . . . . . . . 11 (𝑦 = 𝑆 → ((Lim 𝑦 → (𝐹𝑦) = 𝑥𝑦 (𝐹𝑥)) ↔ (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥))))
40 onfununi.1 . . . . . . . . . . 11 (Lim 𝑦 → (𝐹𝑦) = 𝑥𝑦 (𝐹𝑥))
4139, 40vtoclg 3515 . . . . . . . . . 10 ( 𝑆 ∈ On → (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥)))
4234, 41syl6 35 . . . . . . . . 9 (𝑆𝑇 → (𝑆 ⊆ On → (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥))))
4342imp 410 . . . . . . . 8 ((𝑆𝑇𝑆 ⊆ On) → (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥)))
44433adant3 1129 . . . . . . 7 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥)))
4544adantr 484 . . . . . 6 (((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → (Lim 𝑆 → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥)))
4633, 45mpd 15 . . . . 5 (((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → (𝐹 𝑆) = 𝑥 𝑆(𝐹𝑥))
47 eluni2 4804 . . . . . . . . . . . 12 (𝑥 𝑆 ↔ ∃𝑦𝑆 𝑥𝑦)
48 ssel 3908 . . . . . . . . . . . . . . . . . 18 (𝑆 ⊆ On → (𝑦𝑆𝑦 ∈ On))
4948anim1d 613 . . . . . . . . . . . . . . . . 17 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → (𝑦 ∈ On ∧ 𝑥𝑦)))
50 onelon 6184 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ 𝑥𝑦) → 𝑥 ∈ On)
5149, 50syl6 35 . . . . . . . . . . . . . . . 16 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → 𝑥 ∈ On))
5248adantrd 495 . . . . . . . . . . . . . . . 16 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → 𝑦 ∈ On))
53 eloni 6169 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On → Ord 𝑦)
5448, 53syl6 35 . . . . . . . . . . . . . . . . 17 (𝑆 ⊆ On → (𝑦𝑆 → Ord 𝑦))
55 ordelss 6175 . . . . . . . . . . . . . . . . . 18 ((Ord 𝑦𝑥𝑦) → 𝑥𝑦)
5655a1i 11 . . . . . . . . . . . . . . . . 17 (𝑆 ⊆ On → ((Ord 𝑦𝑥𝑦) → 𝑥𝑦))
5754, 56syland 605 . . . . . . . . . . . . . . . 16 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → 𝑥𝑦))
5851, 52, 573jcad 1126 . . . . . . . . . . . . . . 15 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥𝑦)))
59 onfununi.2 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦))
6058, 59syl6 35 . . . . . . . . . . . . . 14 (𝑆 ⊆ On → ((𝑦𝑆𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦)))
6160expd 419 . . . . . . . . . . . . 13 (𝑆 ⊆ On → (𝑦𝑆 → (𝑥𝑦 → (𝐹𝑥) ⊆ (𝐹𝑦))))
6261reximdvai 3231 . . . . . . . . . . . 12 (𝑆 ⊆ On → (∃𝑦𝑆 𝑥𝑦 → ∃𝑦𝑆 (𝐹𝑥) ⊆ (𝐹𝑦)))
6347, 62syl5bi 245 . . . . . . . . . . 11 (𝑆 ⊆ On → (𝑥 𝑆 → ∃𝑦𝑆 (𝐹𝑥) ⊆ (𝐹𝑦)))
64 ssiun 4933 . . . . . . . . . . 11 (∃𝑦𝑆 (𝐹𝑥) ⊆ (𝐹𝑦) → (𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦))
6563, 64syl6 35 . . . . . . . . . 10 (𝑆 ⊆ On → (𝑥 𝑆 → (𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦)))
6665ralrimiv 3148 . . . . . . . . 9 (𝑆 ⊆ On → ∀𝑥 𝑆(𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦))
67 iunss 4932 . . . . . . . . 9 ( 𝑥 𝑆(𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦) ↔ ∀𝑥 𝑆(𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦))
6866, 67sylibr 237 . . . . . . . 8 (𝑆 ⊆ On → 𝑥 𝑆(𝐹𝑥) ⊆ 𝑦𝑆 (𝐹𝑦))
69 fveq2 6645 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
7069cbviunv 4927 . . . . . . . 8 𝑦𝑆 (𝐹𝑦) = 𝑥𝑆 (𝐹𝑥)
7168, 70sseqtrdi 3965 . . . . . . 7 (𝑆 ⊆ On → 𝑥 𝑆(𝐹𝑥) ⊆ 𝑥𝑆 (𝐹𝑥))
72713ad2ant2 1131 . . . . . 6 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → 𝑥 𝑆(𝐹𝑥) ⊆ 𝑥𝑆 (𝐹𝑥))
7372adantr 484 . . . . 5 (((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → 𝑥 𝑆(𝐹𝑥) ⊆ 𝑥𝑆 (𝐹𝑥))
7446, 73eqsstrd 3953 . . . 4 (((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ 𝑆𝑆) → (𝐹 𝑆) ⊆ 𝑥𝑆 (𝐹𝑥))
7574ex 416 . . 3 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ 𝑆𝑆 → (𝐹 𝑆) ⊆ 𝑥𝑆 (𝐹𝑥)))
76 fveq2 6645 . . . 4 (𝑥 = 𝑆 → (𝐹𝑥) = (𝐹 𝑆))
7776ssiun2s 4935 . . 3 ( 𝑆𝑆 → (𝐹 𝑆) ⊆ 𝑥𝑆 (𝐹𝑥))
7875, 77pm2.61d2 184 . 2 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹 𝑆) ⊆ 𝑥𝑆 (𝐹𝑥))
7934imp 410 . . . . . 6 ((𝑆𝑇𝑆 ⊆ On) → 𝑆 ∈ On)
80793adant3 1129 . . . . 5 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → 𝑆 ∈ On)
8163ad2ant2 1131 . . . . . 6 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥𝑆𝑥 ∈ On))
8281, 4jca2 517 . . . . 5 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥𝑆 → (𝑥 ∈ On ∧ 𝑥 𝑆)))
83 sseq2 3941 . . . . . . . 8 (𝑦 = 𝑆 → (𝑥𝑦𝑥 𝑆))
8483anbi2d 631 . . . . . . 7 (𝑦 = 𝑆 → ((𝑥 ∈ On ∧ 𝑥𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 𝑆)))
8536sseq2d 3947 . . . . . . 7 (𝑦 = 𝑆 → ((𝐹𝑥) ⊆ (𝐹𝑦) ↔ (𝐹𝑥) ⊆ (𝐹 𝑆)))
8684, 85imbi12d 348 . . . . . 6 (𝑦 = 𝑆 → (((𝑥 ∈ On ∧ 𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 𝑆) → (𝐹𝑥) ⊆ (𝐹 𝑆))))
87593com12 1120 . . . . . . 7 ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦))
88873expib 1119 . . . . . 6 (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥𝑦) → (𝐹𝑥) ⊆ (𝐹𝑦)))
8986, 88vtoclga 3522 . . . . 5 ( 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 𝑆) → (𝐹𝑥) ⊆ (𝐹 𝑆)))
9080, 82, 89sylsyld 61 . . . 4 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥𝑆 → (𝐹𝑥) ⊆ (𝐹 𝑆)))
9190ralrimiv 3148 . . 3 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥𝑆 (𝐹𝑥) ⊆ (𝐹 𝑆))
92 iunss 4932 . . 3 ( 𝑥𝑆 (𝐹𝑥) ⊆ (𝐹 𝑆) ↔ ∀𝑥𝑆 (𝐹𝑥) ⊆ (𝐹 𝑆))
9391, 92sylibr 237 . 2 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → 𝑥𝑆 (𝐹𝑥) ⊆ (𝐹 𝑆))
9478, 93eqssd 3932 1 ((𝑆𝑇𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹 𝑆) = 𝑥𝑆 (𝐹𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2111  wne 2987  wral 3106  wrex 3107  wss 3881  c0 4243   cuni 4800   ciun 4881  Ord word 6158  Oncon0 6159  Lim wlim 6160  cfv 6324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-tr 5137  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6162  df-on 6163  df-lim 6164  df-iota 6283  df-fv 6332
This theorem is referenced by:  onovuni  7962
  Copyright terms: Public domain W3C validator