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

Theorem fun11iun 7111
Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)
Hypotheses
Ref Expression
fun11iun.1 (𝑥 = 𝑦𝐵 = 𝐶)
fun11iun.2 𝐵 ∈ V
Assertion
Ref Expression
fun11iun (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷1-1𝑆)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝑆
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑥,𝑦)   𝑆(𝑦)

Proof of Theorem fun11iun
Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3198 . . . . . . . . . 10 𝑢 ∈ V
2 eqeq1 2624 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝑧 = 𝐵𝑢 = 𝐵))
32rexbidv 3048 . . . . . . . . . 10 (𝑧 = 𝑢 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑢 = 𝐵))
41, 3elab 3344 . . . . . . . . 9 (𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑢 = 𝐵)
5 r19.29 3068 . . . . . . . . . 10 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ∃𝑥𝐴 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵))
6 nfv 1841 . . . . . . . . . . . 12 𝑥(Fun 𝑢 ∧ Fun 𝑢)
7 nfre1 3002 . . . . . . . . . . . . . 14 𝑥𝑥𝐴 𝑧 = 𝐵
87nfab 2766 . . . . . . . . . . . . 13 𝑥{𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
9 nfv 1841 . . . . . . . . . . . . 13 𝑥(𝑢𝑣𝑣𝑢)
108, 9nfral 2942 . . . . . . . . . . . 12 𝑥𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)
116, 10nfan 1826 . . . . . . . . . . 11 𝑥((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
12 f1eq1 6083 . . . . . . . . . . . . . . . 16 (𝑢 = 𝐵 → (𝑢:𝐷1-1𝑆𝐵:𝐷1-1𝑆))
1312biimparc 504 . . . . . . . . . . . . . . 15 ((𝐵:𝐷1-1𝑆𝑢 = 𝐵) → 𝑢:𝐷1-1𝑆)
14 df-f1 5881 . . . . . . . . . . . . . . . 16 (𝑢:𝐷1-1𝑆 ↔ (𝑢:𝐷𝑆 ∧ Fun 𝑢))
15 ffun 6035 . . . . . . . . . . . . . . . . 17 (𝑢:𝐷𝑆 → Fun 𝑢)
1615anim1i 591 . . . . . . . . . . . . . . . 16 ((𝑢:𝐷𝑆 ∧ Fun 𝑢) → (Fun 𝑢 ∧ Fun 𝑢))
1714, 16sylbi 207 . . . . . . . . . . . . . . 15 (𝑢:𝐷1-1𝑆 → (Fun 𝑢 ∧ Fun 𝑢))
1813, 17syl 17 . . . . . . . . . . . . . 14 ((𝐵:𝐷1-1𝑆𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun 𝑢))
1918adantlr 750 . . . . . . . . . . . . 13 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun 𝑢))
20 vex 3198 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
21 eqeq1 2624 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑣 → (𝑧 = 𝐵𝑣 = 𝐵))
2221rexbidv 3048 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑣 = 𝐵))
2320, 22elab 3344 . . . . . . . . . . . . . . 15 (𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑣 = 𝐵)
24 fun11iun.1 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦𝐵 = 𝐶)
2524eqeq2d 2630 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑣 = 𝐵𝑣 = 𝐶))
2625cbvrexv 3167 . . . . . . . . . . . . . . . 16 (∃𝑥𝐴 𝑣 = 𝐵 ↔ ∃𝑦𝐴 𝑣 = 𝐶)
27 r19.29 3068 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → ∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶))
28 sseq12 3620 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = 𝐵𝑣 = 𝐶) → (𝑢𝑣𝐵𝐶))
2928ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑢𝑣𝐵𝐶))
30 sseq12 3620 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑣𝑢𝐶𝐵))
3129, 30orbi12d 745 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 = 𝐶𝑢 = 𝐵) → ((𝑢𝑣𝑣𝑢) ↔ (𝐵𝐶𝐶𝐵)))
3231biimprcd 240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵𝐶𝐶𝐵) → ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢)))
3332expdimp 453 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢𝑣𝑣𝑢)))
3433rexlimivw 3025 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢𝑣𝑣𝑢)))
3534imp 445 . . . . . . . . . . . . . . . . . . 19 ((∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢))
3627, 35sylan 488 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢))
3736an32s 845 . . . . . . . . . . . . . . . . 17 (((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ 𝑢 = 𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → (𝑢𝑣𝑣𝑢))
3837adantlll 753 . . . . . . . . . . . . . . . 16 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → (𝑢𝑣𝑣𝑢))
3926, 38sylan2b 492 . . . . . . . . . . . . . . 15 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑥𝐴 𝑣 = 𝐵) → (𝑢𝑣𝑣𝑢))
4023, 39sylan2b 492 . . . . . . . . . . . . . 14 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → (𝑢𝑣𝑣𝑢))
4140ralrimiva 2963 . . . . . . . . . . . . 13 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
4219, 41jca 554 . . . . . . . . . . . 12 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
4342a1i 11 . . . . . . . . . . 11 (𝑥𝐴 → (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))))
4411, 43rexlimi 3020 . . . . . . . . . 10 (∃𝑥𝐴 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
455, 44syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
464, 45sylan2b 492 . . . . . . . 8 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
4746ralrimiva 2963 . . . . . . 7 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
48 fun11uni 7105 . . . . . . 7 (∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)) → (Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ∧ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}))
4947, 48syl 17 . . . . . 6 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ∧ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}))
5049simpld 475 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
51 fun11iun.2 . . . . . . 7 𝐵 ∈ V
5251dfiun2 4545 . . . . . 6 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
5352funeqi 5897 . . . . 5 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
5450, 53sylibr 224 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
55 nfra1 2938 . . . . . . 7 𝑥𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵))
56 rsp 2926 . . . . . . . . 9 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑥𝐴 → (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵))))
571eldm2 5311 . . . . . . . . . . 11 (𝑢 ∈ dom 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝐵)
58 f1dm 6092 . . . . . . . . . . . 12 (𝐵:𝐷1-1𝑆 → dom 𝐵 = 𝐷)
5958eleq2d 2685 . . . . . . . . . . 11 (𝐵:𝐷1-1𝑆 → (𝑢 ∈ dom 𝐵𝑢𝐷))
6057, 59syl5bbr 274 . . . . . . . . . 10 (𝐵:𝐷1-1𝑆 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6160adantr 481 . . . . . . . . 9 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6256, 61syl6 35 . . . . . . . 8 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑥𝐴 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷)))
6362imp 445 . . . . . . 7 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑥𝐴) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6455, 63rexbida 3043 . . . . . 6 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥𝐴 𝑢𝐷))
65 eliun 4515 . . . . . . . 8 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
6665exbii 1772 . . . . . . 7 (∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
671eldm2 5311 . . . . . . 7 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵)
68 rexcom4 3220 . . . . . . 7 (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
6966, 67, 683bitr4i 292 . . . . . 6 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵)
70 eliun 4515 . . . . . 6 (𝑢 𝑥𝐴 𝐷 ↔ ∃𝑥𝐴 𝑢𝐷)
7164, 69, 703bitr4g 303 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑢 ∈ dom 𝑥𝐴 𝐵𝑢 𝑥𝐴 𝐷))
7271eqrdv 2618 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷)
73 df-fn 5879 . . . 4 ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ↔ (Fun 𝑥𝐴 𝐵 ∧ dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷))
7454, 72, 73sylanbrc 697 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷)
75 rniun 5531 . . . 4 ran 𝑥𝐴 𝐵 = 𝑥𝐴 ran 𝐵
76 f1f 6088 . . . . . . . 8 (𝐵:𝐷1-1𝑆𝐵:𝐷𝑆)
77 frn 6040 . . . . . . . 8 (𝐵:𝐷𝑆 → ran 𝐵𝑆)
7876, 77syl 17 . . . . . . 7 (𝐵:𝐷1-1𝑆 → ran 𝐵𝑆)
7978adantr 481 . . . . . 6 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝐵𝑆)
8079ralimi 2949 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑥𝐴 ran 𝐵𝑆)
81 iunss 4552 . . . . 5 ( 𝑥𝐴 ran 𝐵𝑆 ↔ ∀𝑥𝐴 ran 𝐵𝑆)
8280, 81sylibr 224 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 ran 𝐵𝑆)
8375, 82syl5eqss 3641 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝑥𝐴 𝐵𝑆)
84 df-f 5880 . . 3 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ↔ ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ∧ ran 𝑥𝐴 𝐵𝑆))
8574, 83, 84sylanbrc 697 . 2 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
8649simprd 479 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
8752cnveqi 5286 . . . 4 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
8887funeqi 5897 . . 3 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
8986, 88sylibr 224 . 2 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
90 df-f1 5881 . 2 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷1-1𝑆 ↔ ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ∧ Fun 𝑥𝐴 𝐵))
9185, 89, 90sylanbrc 697 1 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷1-1𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wex 1702  wcel 1988  {cab 2606  wral 2909  wrex 2910  Vcvv 3195  wss 3567  cop 4174   cuni 4427   ciun 4511  ccnv 5103  dom cdm 5104  ran crn 5105  Fun wfun 5870   Fn wfn 5871  wf 5872  1-1wf1 5873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881
This theorem is referenced by:  ackbij2  9050
  Copyright terms: Public domain W3C validator