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

Theorem fun11iun 7273
 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 3354 . . . . . . . . . 10 𝑢 ∈ V
2 eqeq1 2775 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝑧 = 𝐵𝑢 = 𝐵))
32rexbidv 3200 . . . . . . . . . 10 (𝑧 = 𝑢 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑢 = 𝐵))
41, 3elab 3501 . . . . . . . . 9 (𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑢 = 𝐵)
5 r19.29 3220 . . . . . . . . . 10 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ∃𝑥𝐴 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵))
6 nfv 1995 . . . . . . . . . . . 12 𝑥(Fun 𝑢 ∧ Fun 𝑢)
7 nfre1 3153 . . . . . . . . . . . . . 14 𝑥𝑥𝐴 𝑧 = 𝐵
87nfab 2918 . . . . . . . . . . . . 13 𝑥{𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
9 nfv 1995 . . . . . . . . . . . . 13 𝑥(𝑢𝑣𝑣𝑢)
108, 9nfral 3094 . . . . . . . . . . . 12 𝑥𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)
116, 10nfan 1980 . . . . . . . . . . 11 𝑥((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
12 f1eq1 6236 . . . . . . . . . . . . . . . 16 (𝑢 = 𝐵 → (𝑢:𝐷1-1𝑆𝐵:𝐷1-1𝑆))
1312biimparc 465 . . . . . . . . . . . . . . 15 ((𝐵:𝐷1-1𝑆𝑢 = 𝐵) → 𝑢:𝐷1-1𝑆)
14 df-f1 6036 . . . . . . . . . . . . . . . 16 (𝑢:𝐷1-1𝑆 ↔ (𝑢:𝐷𝑆 ∧ Fun 𝑢))
15 ffun 6188 . . . . . . . . . . . . . . . . 17 (𝑢:𝐷𝑆 → Fun 𝑢)
1615anim1i 602 . . . . . . . . . . . . . . . 16 ((𝑢:𝐷𝑆 ∧ Fun 𝑢) → (Fun 𝑢 ∧ Fun 𝑢))
1714, 16sylbi 207 . . . . . . . . . . . . . . 15 (𝑢:𝐷1-1𝑆 → (Fun 𝑢 ∧ Fun 𝑢))
1813, 17syl 17 . . . . . . . . . . . . . 14 ((𝐵:𝐷1-1𝑆𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun 𝑢))
1918adantlr 694 . . . . . . . . . . . . 13 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun 𝑢))
20 vex 3354 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
21 eqeq1 2775 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑣 → (𝑧 = 𝐵𝑣 = 𝐵))
2221rexbidv 3200 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑣 = 𝐵))
2320, 22elab 3501 . . . . . . . . . . . . . . 15 (𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑣 = 𝐵)
24 fun11iun.1 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦𝐵 = 𝐶)
2524eqeq2d 2781 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑣 = 𝐵𝑣 = 𝐶))
2625cbvrexv 3321 . . . . . . . . . . . . . . . 16 (∃𝑥𝐴 𝑣 = 𝐵 ↔ ∃𝑦𝐴 𝑣 = 𝐶)
27 r19.29 3220 . . . . . . . . . . . . . . . . . . 19 ((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → ∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶))
28 sseq12 3777 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 = 𝐵𝑣 = 𝐶) → (𝑢𝑣𝐵𝐶))
2928ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑢𝑣𝐵𝐶))
30 sseq12 3777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑣𝑢𝐶𝐵))
3129, 30orbi12d 904 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 = 𝐶𝑢 = 𝐵) → ((𝑢𝑣𝑣𝑢) ↔ (𝐵𝐶𝐶𝐵)))
3231biimprcd 240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐵𝐶𝐶𝐵) → ((𝑣 = 𝐶𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢)))
3332expdimp 440 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢𝑣𝑣𝑢)))
3433rexlimivw 3177 . . . . . . . . . . . . . . . . . . . 20 (∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) → (𝑢 = 𝐵 → (𝑢𝑣𝑣𝑢)))
3534imp 393 . . . . . . . . . . . . . . . . . . 19 ((∃𝑦𝐴 ((𝐵𝐶𝐶𝐵) ∧ 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢))
3627, 35sylan 569 . . . . . . . . . . . . . . . . . 18 (((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) ∧ 𝑢 = 𝐵) → (𝑢𝑣𝑣𝑢))
3736an32s 631 . . . . . . . . . . . . . . . . 17 (((∀𝑦𝐴 (𝐵𝐶𝐶𝐵) ∧ 𝑢 = 𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → (𝑢𝑣𝑣𝑢))
3837adantlll 697 . . . . . . . . . . . . . . . 16 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑦𝐴 𝑣 = 𝐶) → (𝑢𝑣𝑣𝑢))
3926, 38sylan2b 581 . . . . . . . . . . . . . . 15 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ ∃𝑥𝐴 𝑣 = 𝐵) → (𝑢𝑣𝑣𝑢))
4023, 39sylan2b 581 . . . . . . . . . . . . . 14 ((((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → (𝑢𝑣𝑣𝑢))
4140ralrimiva 3115 . . . . . . . . . . . . 13 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
4219, 41jca 501 . . . . . . . . . . . 12 (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
4342a1i 11 . . . . . . . . . . 11 (𝑥𝐴 → (((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))))
4411, 43rexlimi 3172 . . . . . . . . . 10 (∃𝑥𝐴 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
455, 44syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
464, 45sylan2b 581 . . . . . . . 8 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
4746ralrimiva 3115 . . . . . . 7 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
48 fun11uni 7267 . . . . . . 7 (∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun 𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)) → (Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ∧ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}))
4947, 48syl 17 . . . . . 6 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ∧ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}))
5049simpld 482 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
51 fun11iun.2 . . . . . . 7 𝐵 ∈ V
5251dfiun2 4688 . . . . . 6 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
5352funeqi 6052 . . . . 5 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
5450, 53sylibr 224 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
55 nfra1 3090 . . . . . . 7 𝑥𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵))
56 rsp 3078 . . . . . . . . 9 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑥𝐴 → (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵))))
571eldm2 5460 . . . . . . . . . . 11 (𝑢 ∈ dom 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝐵)
58 f1dm 6245 . . . . . . . . . . . 12 (𝐵:𝐷1-1𝑆 → dom 𝐵 = 𝐷)
5958eleq2d 2836 . . . . . . . . . . 11 (𝐵:𝐷1-1𝑆 → (𝑢 ∈ dom 𝐵𝑢𝐷))
6057, 59syl5bbr 274 . . . . . . . . . 10 (𝐵:𝐷1-1𝑆 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6160adantr 466 . . . . . . . . 9 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6256, 61syl6 35 . . . . . . . 8 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑥𝐴 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷)))
6362imp 393 . . . . . . 7 ((∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑥𝐴) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
6455, 63rexbida 3195 . . . . . 6 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥𝐴 𝑢𝐷))
65 eliun 4658 . . . . . . . 8 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
6665exbii 1924 . . . . . . 7 (∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
671eldm2 5460 . . . . . . 7 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵)
68 rexcom4 3377 . . . . . . 7 (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
6966, 67, 683bitr4i 292 . . . . . 6 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵)
70 eliun 4658 . . . . . 6 (𝑢 𝑥𝐴 𝐷 ↔ ∃𝑥𝐴 𝑢𝐷)
7164, 69, 703bitr4g 303 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑢 ∈ dom 𝑥𝐴 𝐵𝑢 𝑥𝐴 𝐷))
7271eqrdv 2769 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷)
73 df-fn 6034 . . . 4 ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ↔ (Fun 𝑥𝐴 𝐵 ∧ dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷))
7454, 72, 73sylanbrc 572 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷)
75 rniun 5684 . . . 4 ran 𝑥𝐴 𝐵 = 𝑥𝐴 ran 𝐵
76 f1f 6241 . . . . . . . 8 (𝐵:𝐷1-1𝑆𝐵:𝐷𝑆)
77 frn 6193 . . . . . . . 8 (𝐵:𝐷𝑆 → ran 𝐵𝑆)
7876, 77syl 17 . . . . . . 7 (𝐵:𝐷1-1𝑆 → ran 𝐵𝑆)
7978adantr 466 . . . . . 6 ((𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝐵𝑆)
8079ralimi 3101 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑥𝐴 ran 𝐵𝑆)
81 iunss 4695 . . . . 5 ( 𝑥𝐴 ran 𝐵𝑆 ↔ ∀𝑥𝐴 ran 𝐵𝑆)
8280, 81sylibr 224 . . . 4 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 ran 𝐵𝑆)
8375, 82syl5eqss 3798 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝑥𝐴 𝐵𝑆)
84 df-f 6035 . . 3 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ↔ ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ∧ ran 𝑥𝐴 𝐵𝑆))
8574, 83, 84sylanbrc 572 . 2 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
8649simprd 483 . . 3 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
8752cnveqi 5435 . . . 4 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
8887funeqi 6052 . . 3 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
8986, 88sylibr 224 . 2 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
90 df-f1 6036 . 2 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷1-1𝑆 ↔ ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ∧ Fun 𝑥𝐴 𝐵))
9185, 89, 90sylanbrc 572 1 (∀𝑥𝐴 (𝐵:𝐷1-1𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷1-1𝑆)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 836   = wceq 1631  ∃wex 1852   ∈ wcel 2145  {cab 2757  ∀wral 3061  ∃wrex 3062  Vcvv 3351   ⊆ wss 3723  ⟨cop 4322  ∪ cuni 4574  ∪ ciun 4654  ◡ccnv 5248  dom cdm 5249  ran crn 5250  Fun wfun 6025   Fn wfn 6026  ⟶wf 6027  –1-1→wf1 6028 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036 This theorem is referenced by:  ackbij2  9267
 Copyright terms: Public domain W3C validator